diff --git a/SPEC_FORMAT.md b/SPEC_FORMAT.md
index 6a3de99c5869fe28a967267a942fc16de3f78f3b..39f41eb8034134eceb9fe6b0944084ebe59648cf 100644
--- a/SPEC_FORMAT.md
+++ b/SPEC_FORMAT.md
@@ -47,6 +47,43 @@ There are further attributes that influence the proof-checking behaviour:
| `skip` | ignore annotations on this function completely | none | `#[rr::skip]` |
| `export_as` | influence the exported path in the generated RefinedRust library interface for import in other proofs | a Rust path | `#[rr::export_as(std::vec::Vec::push)]` |
+## Closure attributes
+RefinedRust has experimental support for closures.
+The same attributs as for functions apply, but in addition, you can specify assumptions and modifications on the captures of the closure using the `rr::capture` attribute.
+
+It semantics are best understood using some examples:
+```
+let x = 5;
+
+let clos =
+ #[rr::params("i")]
+ #[rr::capture("x": "i")]
+ #[rr::requires("(2 * i)%Z ∈ i32")]
+ #[rr::returns("(2 * i)%Z")]
+ || {
+ x * 2
+ };
+```
+In this example, the variable `x` is captured as a shared reference.
+Hence, the `rr::capture` attribute specifies that we assume the captured value of `x` to have refinement `i`.
+
+The same applies for move-captured variables.
+
+For mutably captured variables, we can also specify the new value after the closure returns (separated by `->`), as in the following example:
+```
+let mut y = 2;
+
+let mut clos =
+ #[rr::params("i")]
+ #[rr::capture("y": "i" -> "(2*i)%Z")]
+ #[rr::requires("(2 * i)%Z ∈ i32")]
+ || { y *= 2; };
+```
+Currently, RefinedRust does not support the case that only a subplace of a variable is captured very well.
+For references of which a subplace is captured, the capture specification implicitly applies to the actually captured subplace, while other cases are not supported.
+In the future, the specification language will be extended to handle these cases better.
+
+
## Impl attributes
The following attributes are also available on impls and then influence all functions contained in them:
| Keyword | Purpose | Properties | Example |
diff --git a/case_studies/tests/src/closures.rs b/case_studies/tests/src/closures.rs
new file mode 100644
index 0000000000000000000000000000000000000000..b2708f93b90b5dedee215457ade3dfc081afec56
--- /dev/null
+++ b/case_studies/tests/src/closures.rs
@@ -0,0 +1,124 @@
+#[rr::returns("()")]
+fn closure_test1() {
+
+ // Fn-closure
+ let x =
+ #[rr::params("i")]
+ #[rr::args("i")]
+ #[rr::requires("(2 * i)%Z ∈ i32")]
+ #[rr::returns("(2 * i)%Z")]
+ |x: i32| {
+ x * 2
+ };
+
+ // here we call the closure's implementation
+ //x(2);
+}
+
+#[rr::returns("()")]
+fn closure_test5() {
+ let x = 5;
+
+ // Fn-closure
+ let x =
+ #[rr::params("i")]
+ #[rr::capture("x": "i")]
+ #[rr::requires("(2 * i)%Z ∈ i32")]
+ #[rr::returns("(2 * i)%Z")]
+ || {
+ x * 2
+ };
+
+ // here we call the closure's implementation
+ //x(2);
+}
+
+/*
+#[rr::params("x")]
+#[rr::args("#x")]
+#[rr::returns("()")]
+fn closure_test6(z: &i32) {
+ let x = 5;
+
+ // Fn-closure
+ let x =
+ #[rr::params("i", "j")]
+ #[rr::capture("x": "i")]
+ #[rr::capture("z": "j")]
+ #[rr::requires("(j * i)%Z ∈ i32")]
+ #[rr::returns("(j * i)%Z")]
+ || {
+ x * z
+ };
+
+ // here we call the closure's implementation
+ //x(2);
+}
+*/
+
+#[rr::returns("()")]
+fn closure_test2() {
+ let mut y = 2;
+
+ // here, we prove initialization of the closure
+
+ let mut x =
+ // Note: the closure code has a doubly-nested mutable references, since it gets a mutref to
+ // the capture also.
+ #[rr::params("i")]
+ #[rr::capture("y": "i" -> "(2*i)%Z")]
+ #[rr::requires("(2 * i)%Z ∈ i32")]
+ || { y *= 2; };
+
+ //x();
+ //x();
+
+ // here, we deinitialize the closure
+ y = y + 1;
+}
+
+#[rr::params("a", "γ")]
+#[rr::args("(#a, γ)")]
+#[rr::requires("(4*a)%Z ∈ i32")]
+//#[rr::observe("γ" : "(4 * a)%Z")]
+#[rr::observe("γ" : "a")]
+#[rr::returns("()")]
+#[rr::tactics("unsafe_unfold_common_caesium_defs; solve_goal.")]
+fn closure_test3(y: &mut i32) {
+ let mut z = 5;
+ let mut yy = 423;
+
+ let mut x =
+ // this effectively takes a mutable reference for initialization
+ #[rr::params("i", "j")]
+ // TODO: we should specify the projection here.
+ #[rr::capture("y" : "i" -> "2*i")]
+ #[rr::capture("z" : "j" -> "5*j")]
+ #[rr::requires("(2 * i)%Z ∈ i32")]
+ #[rr::requires("(5 * j)%Z ∈ i32")]
+ || { *y *= 2; z *= 5; };
+
+ //x();
+ //x();
+}
+
+/*
+#[rr::returns("()")]
+fn closure_test4(y: &mut i32) {
+ let mut z = 5;
+
+ let mut x =
+ // this effectively takes a mutable reference for initialization
+ #[rr::params("i", "γ", "j", "γj")]
+ #[rr::capture_pre("y" : "(i, γ)")]
+ #[rr::capture_pre("z" : "(j, γj)")]
+ #[rr::capture_post("y" : "(2*i, γ)")]
+ #[rr::capture_post("z" : "(5*i, γj)")]
+ |x: &mut i32, w: &mut i32| { *y *= z; *x *= *w; };
+}
+*/
+
+
+// Note: probably I could try to have a more creusot-like language that compiles down to this
+// representation
+
diff --git a/case_studies/tests/src/lib.rs b/case_studies/tests/src/lib.rs
index 01cb8147d1b28ae9656d997f9aa02f77bdd4989f..4a36f9e1aeb88bfc5d76c23abc960b9ebf12adf4 100644
--- a/case_studies/tests/src/lib.rs
+++ b/case_studies/tests/src/lib.rs
@@ -1,6 +1,7 @@
#![feature(register_tool)]
#![register_tool(rr)]
#![feature(custom_inner_attributes)]
+#![feature(stmt_expr_attributes)]
mod enums;
mod structs;
@@ -9,3 +10,6 @@ mod traits;
mod statics;
mod vec_client;
+mod mixed;
+mod closures;
+mod references;
diff --git a/case_studies/tests/src/mixed.rs b/case_studies/tests/src/mixed.rs
new file mode 100644
index 0000000000000000000000000000000000000000..d6613cbb59eaffc6d413a5b93f55f97f8c6e5e30
--- /dev/null
+++ b/case_studies/tests/src/mixed.rs
@@ -0,0 +1,18 @@
+
+#[macro_export]
+macro_rules! rr_stop {
+ ( ) => {
+ #[allow(unused_variables)]
+ let _ = #[rr::ignore] || {};
+ };
+}
+
+#[rr::returns("()")]
+fn test_mixed() {
+ let mut x = 4;
+ //rr_stop!();
+ let mut y = 5;
+ x = 10;
+ //rr_stop!();
+ y = 20;
+}
diff --git a/case_studies/tests/src/references.rs b/case_studies/tests/src/references.rs
new file mode 100644
index 0000000000000000000000000000000000000000..ad685284e607148d911ab3f4905cd2941015ccd3
--- /dev/null
+++ b/case_studies/tests/src/references.rs
@@ -0,0 +1,16 @@
+
+#[rr::params("γ1", "γ2", "i")]
+#[rr::args("(#(#i, γ1), γ2)")]
+#[rr::observe("γ2": "(#i, γ1)")]
+#[rr::returns("i")]
+fn mut_ref_test1(x: &mut &mut i32) -> i32 {
+ **x
+}
+
+#[rr::params("γ1", "γ2", "i", "j")]
+#[rr::args("(#(-[#(#i, γ1); #j]), γ2)")]
+#[rr::observe("γ2": "(-[#(#i, γ1); #j])")]
+#[rr::returns("i")]
+fn mut_ref_test2(x: &mut (&mut i32, i32)) -> i32 {
+ *((*x).0)
+}
diff --git a/case_studies/tests/src/traits.rs b/case_studies/tests/src/traits.rs
index 7502bab1e145ad952b0590e14cc919ba6fc24469..ea7b7396dc3a3f00cc1f872a3f7b9a8930e043c6 100644
--- a/case_studies/tests/src/traits.rs
+++ b/case_studies/tests/src/traits.rs
@@ -1,3 +1,4 @@
+
trait MyAdd {
fn my_add(x: Self, y: Self) -> Self;
}
@@ -16,3 +17,8 @@ impl MyAdd for usize {
fn test_add() {
MyAdd::my_add(5usize, 5usize);
}
+
+#[rr::returns("()")]
+fn test_add_2<T>(x: T, y: T) where T: MyAdd {
+ MyAdd::my_add(x, y);
+}
diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs
index 16b29a8d3d9f44d2758992300b82f98ed10c3c46..bb0f27f44db0abcb45e1d621a2c3802de065e52c 100644
--- a/rr_frontend/radium/src/code.rs
+++ b/rr_frontend/radium/src/code.rs
@@ -502,7 +502,7 @@ impl fmt::Display for Annotation {
write!(f, "CopyLftNameAnnot \"{}\" \"{}\"", lft2, lft1)
},
Self::AliasLftIntersection(lft, lfts) => {
- write!(f, "AliasLftAnnot {} [", lft)?;
+ write!(f, "AliasLftAnnot \"{}\" [", lft)?;
fmt_list(f, lfts, "; ", "\"")?;
write!(f, "]")
},
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index ae25e1c3c842a560ab1ff3d031b57c08683e8620..337dce8a66d80afdca7203ff2b2dd2d7e7458f69 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -16,7 +16,7 @@ pub use crate::coq::*;
#[derive(Clone, Debug, PartialEq)]
/// Encodes a RR type with an accompanying refinement.
-pub struct TypeWithRef<'def>(Type<'def>, String);
+pub struct TypeWithRef<'def>(pub Type<'def>, pub String);
impl<'def> Display for TypeWithRef<'def> {
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), fmt::Error> {
diff --git a/rr_frontend/translation/src/base.rs b/rr_frontend/translation/src/base.rs
index c1a8c8a6176e4a2a68c0dfc1f4be2f54037dfadd..127c1c1890ca901fe6ec60b9ac2160627db4fd2a 100644
--- a/rr_frontend/translation/src/base.rs
+++ b/rr_frontend/translation/src/base.rs
@@ -29,4 +29,5 @@ pub enum TranslationError {
AttributeError(String),
UnknownAttributeParser(String),
UnknownProcedure(String),
+ TraitResolution(String),
}
diff --git a/rr_frontend/translation/src/environment/dump_borrowck_info.rs b/rr_frontend/translation/src/environment/dump_borrowck_info.rs
index b03bc06a4ca10164bb7adb98ce7cce888c0d476b..ec43f3ad3b095d6a07f6d190eaec614ebdf3a589 100644
--- a/rr_frontend/translation/src/environment/dump_borrowck_info.rs
+++ b/rr_frontend/translation/src/environment/dump_borrowck_info.rs
@@ -332,7 +332,8 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> {
if let Some(local) = place.as_local() {
var_names.insert(local, info.name);
} else {
- unimplemented!();
+ var_names.insert(place.local, info.name);
+ //unimplemented!();
}
} else {
unimplemented!();
diff --git a/rr_frontend/translation/src/environment/polonius_info.rs b/rr_frontend/translation/src/environment/polonius_info.rs
index 635105751e7af368c59c0d8f3fa389e20b614aee..1229624e0dd493dc26675eea760eb0bfc7d7ac09 100644
--- a/rr_frontend/translation/src/environment/polonius_info.rs
+++ b/rr_frontend/translation/src/environment/polonius_info.rs
@@ -597,6 +597,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
// TODO check if this does the right thing
return RegionKind::Universal(UniversalRegionKind::Function);
} else {
+ // TODO: this ignores external regions
return RegionKind::Universal(UniversalRegionKind::Local);
}
}
diff --git a/rr_frontend/translation/src/environment/procedure.rs b/rr_frontend/translation/src/environment/procedure.rs
index 2e98c0cbdfd65d336f6ca290afb8aadd488aa874..4baa2ec8b45834bd9e02ade29db867df40ebd5de 100644
--- a/rr_frontend/translation/src/environment/procedure.rs
+++ b/rr_frontend/translation/src/environment/procedure.rs
@@ -47,6 +47,14 @@ impl<'tcx> Procedure<'tcx> {
let ty = tcx.type_of(proc_def_id).instantiate_identity();
let ty_params = match ty.kind() {
ty::TyKind::FnDef(_, params) => params,
+ ty::TyKind::Closure(_, closure_args) => {
+ assert!(ty.is_closure());
+ let clos = closure_args.as_closure();
+ let parent_args = clos.parent_args();
+
+ // TODO: this doesn't include lifetime parameters specific to this closure...
+ tcx.mk_args(parent_args)
+ },
_ => panic!("Procedure::new called on a procedure whose type is not TyKind::FnDef!"),
};
diff --git a/rr_frontend/translation/src/function_body.rs b/rr_frontend/translation/src/function_body.rs
index d33b3993806364fcfd7b7064b666ab2a6b13abff..c8062af43869d76339b77b812961eb227547d53b 100644
--- a/rr_frontend/translation/src/function_body.rs
+++ b/rr_frontend/translation/src/function_body.rs
@@ -6,7 +6,7 @@
use std::collections::{BTreeMap, HashMap, HashSet};
-use log::{info, warn};
+use log::{info, trace, warn};
use radium;
use rustc_ast::ast::Attribute;
use rustc_hir::def_id::DefId;
@@ -29,7 +29,9 @@ use crate::environment::procedure::Procedure;
use crate::environment::{polonius_info as info, Environment};
use crate::inclusion_tracker::*;
use crate::rustc_middle::ty::TypeFoldable;
-use crate::spec_parsers::verbose_function_spec_parser::{FunctionSpecParser, VerboseFunctionSpecParser};
+use crate::spec_parsers::verbose_function_spec_parser::{
+ ClosureMetaInfo, FunctionSpecParser, VerboseFunctionSpecParser,
+};
use crate::type_translator::*;
use crate::tyvars::*;
@@ -201,17 +203,124 @@ pub struct FunctionTranslator<'a, 'def, 'tcx> {
info: &'a PoloniusInfo<'a, 'tcx>,
/// translator for types
ty_translator: &'a TypeTranslator<'def, 'tcx>,
-
- /// inputs of the function, with both early and late bound regions substituted with their
- /// Polonius ReVar
- inputs: Vec<Ty<'tcx>>,
- /// output of the function, similarly with substituted regions
- output: Ty<'tcx>,
}
impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
- /// Translate the body of a function.
- pub fn new(
+ pub fn process_lifetimes_of_args(
+ env: &Environment<'tcx>,
+ params: &[ty::GenericArg<'tcx>],
+ sig: ty::Binder<'tcx, ty::FnSig<'tcx>>,
+ _body: &mir::Body<'tcx>,
+ ) -> (Vec<ty::Ty<'tcx>>, ty::Ty<'tcx>, HashMap<ty::RegionVid, (String, Option<String>)>) {
+ let mut universal_lifetimes = HashMap::new();
+
+ // we create a substitution that replaces early bound regions with their Polonius
+ // region variables
+ let mut subst_early_bounds: Vec<ty::GenericArg<'tcx>> = Vec::new();
+ let mut num_early_bounds = 0;
+ for a in params.iter() {
+ match a.unpack() {
+ ty::GenericArgKind::Lifetime(r) => {
+ // skip over 0 = static
+ let next_id = ty::RegionVid::from_u32(num_early_bounds + 1);
+ let revar = ty::Region::new_var(env.tcx(), next_id);
+ num_early_bounds += 1;
+ subst_early_bounds.push(ty::GenericArg::from(revar));
+
+ match *r {
+ ty::RegionKind::ReEarlyBound(r) => {
+ let name = strip_coq_ident(r.name.as_str());
+ universal_lifetimes.insert(next_id, (format!("ulft_{}", name), Some(name)));
+ },
+ _ => {
+ universal_lifetimes.insert(next_id, (format!("ulft_{}", num_early_bounds), None));
+ },
+ }
+ //println!("early region {}", r);
+ },
+ _ => {
+ subst_early_bounds.push(*a);
+ },
+ }
+ }
+ let subst_early_bounds = env.tcx().mk_args(&subst_early_bounds);
+
+ // add names for late bound region variables
+ let mut num_late_bounds = 0;
+ for b in sig.bound_vars().iter() {
+ let next_id = ty::RegionVid::from_u32(num_early_bounds + num_late_bounds + 1);
+ match b {
+ ty::BoundVariableKind::Region(r) => {
+ match r {
+ ty::BoundRegionKind::BrNamed(_, sym) => {
+ let mut region_name = strip_coq_ident(sym.as_str());
+ if region_name == "_" {
+ region_name = format!("{}", next_id.as_usize());
+ universal_lifetimes.insert(next_id, (format!("ulft_{}", region_name), None));
+ } else {
+ universal_lifetimes
+ .insert(next_id, (format!("ulft_{}", region_name), Some(region_name)));
+ }
+ },
+ ty::BoundRegionKind::BrAnon(_) => {
+ universal_lifetimes
+ .insert(next_id, (format!("ulft_{}", next_id.as_usize()), None));
+ },
+ _ => (),
+ }
+ num_late_bounds += 1;
+ },
+ _ => (),
+ }
+ }
+
+ // replace late-bound region variables by re-enumerating them in the same way as the MIR
+ // type checker does (that this happens in the same way is important to make the names
+ // line up!)
+ let mut next_index = num_early_bounds + 1; // skip over one additional due to static
+ let mut folder = |_| {
+ let cur_index = next_index;
+ next_index += 1;
+ ty::Region::new_var(env.tcx(), ty::RegionVid::from_u32(cur_index))
+ };
+ let (late_sig, _late_region_map) = env.tcx().replace_late_bound_regions(sig, &mut folder);
+
+ // replace early bound variables
+ let inputs: Vec<_> = late_sig
+ .inputs()
+ .iter()
+ .map(|ty| ty_instantiate(*ty, env.tcx(), subst_early_bounds))
+ .collect();
+
+ let output = ty_instantiate(late_sig.output(), env.tcx(), subst_early_bounds);
+
+ (inputs, output, universal_lifetimes)
+ }
+
+ /// At the start of the function, there's a universal (placeholder) region for reference argument.
+ /// These get subsequently relabeled.
+ /// Given the relabeled region, find the original placeholder region.
+ fn find_placeholder_region_for(r: ty::RegionVid, info: &PoloniusInfo) -> Option<ty::RegionVid> {
+ let root_location = Location {
+ block: BasicBlock::from_u32(0),
+ statement_index: 0,
+ };
+ let root_point = info.interner.get_point_index(&facts::Point {
+ location: root_location,
+ typ: facts::PointType::Start,
+ });
+
+ for (ref r1, ref r2, ref p) in info.borrowck_in_facts.subset_base.iter() {
+ if *p == root_point && *r2 == r {
+ info!("find placeholder region for: {:?} ⊑ {:?} = r = {:?}", r1, r2, r);
+ return Some(*r1);
+ }
+ }
+ None
+ }
+
+ /// Create a translation instance for a closure.
+ pub fn new_closure(
env: &'def Environment<'tcx>,
meta: ProcedureMeta,
proc: Procedure<'tcx>,
@@ -224,119 +333,161 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
// TODO can we avoid the leak
let proc: &'def Procedure = &*Box::leak(Box::new(proc));
+ let body = proc.get_mir();
+ Self::dump_body(&body);
+
+ let closure_kind;
let ty: ty::EarlyBinder<Ty<'tcx>> = env.tcx().type_of(proc.get_id());
let ty = ty.instantiate_identity();
- let (sig, substs) = match ty.kind() {
- TyKind::FnDef(_def, args) => {
- assert!(ty.is_fn());
- let sig = ty.fn_sig(env.tcx());
- (sig, args)
+ match ty.kind() {
+ TyKind::Closure(_def, closure_args) => {
+ assert!(ty.is_closure());
+ let clos = closure_args.as_closure();
+
+ closure_kind = clos.kind();
},
- _ => panic!("can not handle non-fns"),
+ _ => panic!("can not handle non-closures"),
};
+ let local_decls = &body.local_decls;
+ let closure_arg = local_decls.get(Local::from_usize(1)).unwrap();
+ let closure_ty;
+
+ match closure_kind {
+ ty::ClosureKind::Fn => {
+ if let ty::TyKind::Ref(_, ty, _) = closure_arg.ty.kind() {
+ closure_ty = ty;
+ } else {
+ unreachable!();
+ }
+ },
+ ty::ClosureKind::FnMut => {
+ if let ty::TyKind::Ref(_, ty, _) = closure_arg.ty.kind() {
+ closure_ty = ty;
+ } else {
+ unreachable!("unexpected type {:?}", closure_arg.ty);
+ }
+ },
+ ty::ClosureKind::FnOnce => {
+ closure_ty = &closure_arg.ty;
+ },
+ }
+
+ let parent_args;
+ let mut capture_regions = Vec::new();
+ let sig;
+ let captures;
+ let upvars_tys;
+ if let ty::TyKind::Closure(did, closure_args) = closure_ty.kind() {
+ let clos = closure_args.as_closure();
+
+ let tupled_upvars_tys = clos.tupled_upvars_ty();
+ upvars_tys = clos.upvar_tys();
+ parent_args = clos.parent_args();
+ sig = clos.sig();
+ info!("closure sig: {:?}", sig);
+
+ captures = env.tcx().closure_captures(did.as_local().unwrap());
+ info!("Closure has captures: {:?}", captures);
+
+ // find additional lifetime parameters
+ for (place, ty) in captures.iter().zip(clos.upvar_tys().iter()) {
+ if let Some(_) = place.region {
+ // find region from ty
+ if let ty::TyKind::Ref(region, _, _) = ty.kind() {
+ capture_regions.push(*region);
+ }
+ }
+ }
+ info!("Closure capture regions: {:?}", capture_regions);
+
+ info!("Closure arg upvar_tys: {:?}", tupled_upvars_tys);
+ info!("Function signature: {:?}", sig);
+ info!("Closure generic args: {:?}", parent_args);
+ } else {
+ unreachable!();
+ }
+
match PoloniusInfo::new(env, proc) {
Ok(info) => {
// TODO: avoid leak
let info: &'def PoloniusInfo = &*Box::leak(Box::new(info));
- let params = proc.get_type_params();
+ // For closures, we only handle the parent's args here!
+ // TODO: do we need to do something special for the parent's late-bound region
+ // parameters?
+ let params = parent_args;
+ //proc.get_type_params();
+ info!("Function generic args: {:?}", params);
// dump graphviz files
// color code: red: dying loan, pink: becoming a zombie; green: is zombie
- crate::environment::dump_borrowck_info(&*env, &proc.get_id(), &info);
+ if rrconfig::dump_borrowck_info() {
+ crate::environment::dump_borrowck_info(&*env, &proc.get_id(), &info);
+ }
- let mut universal_lifetimes = HashMap::new();
+ let (tupled_inputs, output, mut universal_lifetimes) =
+ Self::process_lifetimes_of_args(&env, params, sig, body);
- // we create a substitution that replaces early bound regions with their Polonius
- // region variables
- let mut subst_early_bounds: Vec<ty::GenericArg<'tcx>> = Vec::new();
- let mut num_early_bounds = 0;
- for a in params.iter() {
- match a.unpack() {
- ty::GenericArgKind::Lifetime(r) => {
- // skip over 0 = static
- let next_id = ty::RegionVid::from_u32(num_early_bounds + 1);
- let revar = ty::Region::new_var(env.tcx(), next_id);
- num_early_bounds += 1;
- subst_early_bounds.push(ty::GenericArg::from(revar));
-
- match *r {
- ty::RegionKind::ReEarlyBound(r) => {
- let name = strip_coq_ident(r.name.as_str());
- universal_lifetimes
- .insert(next_id, (format!("ulft_{}", name), Some(name)));
- },
- _ => {
- universal_lifetimes
- .insert(next_id, (format!("ulft_{}", num_early_bounds), None));
- },
- }
- //println!("early region {}", r);
- },
- _ => {
- subst_early_bounds.push(a);
- },
+ // Process the lifetime parameters that come from the captures
+ for r in capture_regions {
+ if let ty::RegionKind::ReVar(r) = r.kind() {
+ let name = format!("ulft_{}", r.as_usize());
+ universal_lifetimes.insert(r, (name, None));
+ } else {
+ unreachable!();
}
}
- let subst_early_bounds = env.tcx().mk_args(&subst_early_bounds);
-
- // add names for late bound region variables
- let mut num_late_bounds = 0;
- for b in sig.bound_vars().iter() {
- let next_id = ty::RegionVid::from_u32(num_early_bounds + num_late_bounds + 1);
- match b {
- ty::BoundVariableKind::Region(r) => {
- match r {
- ty::BoundRegionKind::BrNamed(_, sym) => {
- let mut region_name = strip_coq_ident(sym.as_str());
- if region_name == "_" {
- region_name = format!("{}", next_id.as_usize());
- universal_lifetimes
- .insert(next_id, (format!("ulft_{}", region_name), None));
- } else {
- universal_lifetimes.insert(
- next_id,
- (format!("ulft_{}", region_name), Some(region_name)),
- );
- }
- },
- ty::BoundRegionKind::BrAnon(_) => {
- universal_lifetimes
- .insert(next_id, (format!("ulft_{}", next_id.as_usize()), None));
- },
- _ => (),
- }
- num_late_bounds += 1;
- },
- _ => (),
+ // also add the lifetime for the outer reference
+ let mut maybe_outer_lifetime = None;
+ if let ty::TyKind::Ref(r, _, _) = closure_arg.ty.kind() {
+ if let ty::RegionKind::ReVar(r) = r.kind() {
+ // We need to do some hacks here to find the right Polonius region:
+ // `r` is the non-placeholder region that the variable gets, but we are
+ // looking for the corresponding placeholder region
+ let r2 = Self::find_placeholder_region_for(r, info).unwrap();
+
+ info!("using lifetime {:?} for closure universal", r2);
+ let name = format!("ulft_{}", r2.as_usize());
+ universal_lifetimes.insert(r2, (name, None));
+
+ maybe_outer_lifetime = Some(r2);
+ } else {
+ unreachable!();
}
}
- // replace late-bound region variables by re-enumerating them in the same way as the MIR
- // type checker does (that this happens in the same way is important to make the names
- // line up!)
- let mut next_index = num_early_bounds + 1; // skip over one additional due to static
- let mut folder = |_| {
- let cur_index = next_index;
- next_index += 1;
- ty::Region::new_var(env.tcx(), ty::RegionVid::from_u32(cur_index))
- };
- let (late_sig, _late_region_map) = env.tcx().replace_late_bound_regions(sig, &mut folder);
+ // detuple the inputs
+ assert!(tupled_inputs.len() == 1);
+ let input_tuple_ty = tupled_inputs[0];
+ let mut inputs = Vec::new();
+
+ // push the closure as the first argument
+ /*
+ if let Some(r2) = maybe_outer_lifetime {
+ // in this case, we need to patch the region first
+ if let ty::TyKind::Ref(_, ty, m) = closure_arg.ty.kind() {
+ let new_region = ty::Region::new_var(env.tcx(), r2);
+ inputs.push(env.tcx().mk_ty_from_kind(ty::TyKind::Ref(new_region, *ty, *m)));
+ }
+ }
+ else {
+ inputs.push(closure_arg.ty);
+ }
+ */
- // replace early bound variables
- let inputs: Vec<_> = late_sig
- .inputs()
- .iter()
- .map(|ty| ty_instantiate(*ty, env.tcx(), subst_early_bounds))
- .collect();
- let output = ty_instantiate(late_sig.output(), env.tcx(), subst_early_bounds);
+ if let ty::TyKind::Tuple(args) = input_tuple_ty.kind() {
+ inputs.extend(args.iter());
+ }
+ info!("inputs({}): {:?}, output: {:?}", inputs.len(), inputs, output);
info!("Have lifetime parameters: {:?}", universal_lifetimes);
// add universal lifetimes to the spec
for (_, (lft, name)) in universal_lifetimes.iter() {
+ //let lft = info::AtomicRegion::Universal(info::UniversalRegionKind::Local,
+ // ty::RegionVid::from_u32(1+r));
translated_fn
.add_universal_lifetime(name.clone(), lft.to_string())
.map_err(|e| TranslationError::UnknownError(e))?;
@@ -357,8 +508,9 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
}
// enter the procedure
- let universal_lifetimes: Vec<_> = universal_lifetimes.into_iter().map(|(x, y)| y.0).collect();
- ty_translator.enter_procedure(¶ms, universal_lifetimes)?;
+ let universal_lifetime_map: HashMap<_, _> =
+ universal_lifetimes.into_iter().map(|(x, y)| (x, y.0)).collect();
+ ty_translator.enter_procedure(env.tcx().mk_args(params), universal_lifetime_map)?;
// add generic args to the fn
let generics = ty_translator.generic_scope.borrow();
for t in generics.iter() {
@@ -367,7 +519,134 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
}
}
- let t = Self {
+ let mut t = Self {
+ env,
+ proc,
+ info,
+ translated_fn,
+ inclusion_tracker,
+ procedure_registry: proc_registry,
+ attrs,
+ ty_translator,
+ const_registry,
+ };
+
+ // add universal constraints
+ let universal_constraints = t.get_relevant_universal_constraints();
+ info!("univeral constraints: {:?}", universal_constraints);
+ for (lft1, lft2) in universal_constraints.into_iter() {
+ t.translated_fn
+ .add_universal_lifetime_constraint(lft1, lft2)
+ .map_err(|e| TranslationError::UnknownError(e))?;
+ }
+
+ // compute meta information needed to generate the spec
+ let mut translated_upvars_types = Vec::new();
+ for ty in upvars_tys {
+ let translated_ty = t.ty_translator.translate_type(&ty)?;
+ translated_upvars_types.push(translated_ty);
+ }
+ let meta = ClosureMetaInfo {
+ kind: closure_kind,
+ captures,
+ capture_tys: &translated_upvars_types,
+ closure_lifetime: maybe_outer_lifetime
+ .map(|x| t.ty_translator.lookup_universal_region(x).unwrap()),
+ };
+
+ // process attributes
+ t.process_closure_attrs(&inputs, &output, meta)?;
+ Ok(t)
+ },
+ Err(err) => Err(TranslationError::UnknownError(format!("{:?}", err))),
+ }
+ }
+
+ /// Translate the body of a function.
+ pub fn new(
+ env: &'def Environment<'tcx>,
+ meta: ProcedureMeta,
+ proc: Procedure<'tcx>,
+ attrs: &'a [&'a rustc_ast::ast::AttrItem],
+ ty_translator: &'def TypeTranslator<'def, 'tcx>,
+ proc_registry: &'a ProcedureScope<'def>,
+ const_registry: &'a ConstScope<'def>,
+ ) -> Result<Self, TranslationError> {
+ let mut translated_fn = radium::FunctionBuilder::new(&meta.name, &meta.spec_name);
+
+ // TODO can we avoid the leak
+ let proc: &'def Procedure = &*Box::leak(Box::new(proc));
+
+ let body = proc.get_mir();
+ Self::dump_body(&body);
+
+ let ty: ty::EarlyBinder<Ty<'tcx>> = env.tcx().type_of(proc.get_id());
+ let ty = ty.instantiate_identity();
+ // substs are the generic args of this function (including lifetimes)
+ // sig is the function signature
+ let sig = match ty.kind() {
+ TyKind::FnDef(_def, _args) => {
+ assert!(ty.is_fn());
+ let sig = ty.fn_sig(env.tcx());
+ sig
+ },
+ _ => panic!("can not handle non-fns"),
+ };
+
+ info!("Function signature: {:?}", sig);
+
+ match PoloniusInfo::new(env, proc) {
+ Ok(info) => {
+ // TODO: avoid leak
+ let info: &'def PoloniusInfo = &*Box::leak(Box::new(info));
+
+ let params = proc.get_type_params();
+ info!("Function generic args: {:?}", params);
+
+ // dump graphviz files
+ // color code: red: dying loan, pink: becoming a zombie; green: is zombie
+ if rrconfig::dump_borrowck_info() {
+ crate::environment::dump_borrowck_info(&*env, &proc.get_id(), &info);
+ }
+
+ let (inputs, output, universal_lifetimes) =
+ Self::process_lifetimes_of_args(&env, params, sig, &body);
+ info!("Have lifetime parameters: {:?}", universal_lifetimes);
+
+ // add universal lifetimes to the spec
+ for (_, (lft, name)) in universal_lifetimes.iter() {
+ translated_fn
+ .add_universal_lifetime(name.clone(), lft.to_string())
+ .map_err(|e| TranslationError::UnknownError(e))?;
+ }
+
+ let mut inclusion_tracker = InclusionTracker::new(info);
+ // add placeholder subsets
+ let initial_point: facts::Point = facts::Point {
+ location: BasicBlock::from_u32(0).start_location(),
+ typ: facts::PointType::Start,
+ };
+ for (r1, r2) in info.borrowck_in_facts.known_placeholder_subset.iter() {
+ inclusion_tracker.add_static_inclusion(
+ *r1,
+ *r2,
+ info.interner.get_point_index(&initial_point),
+ );
+ }
+
+ // enter the procedure
+ let universal_lifetime_map: HashMap<_, _> =
+ universal_lifetimes.into_iter().map(|(x, y)| (x, y.0)).collect();
+ ty_translator.enter_procedure(¶ms, universal_lifetime_map)?;
+ // add generic args to the fn
+ let generics = ty_translator.generic_scope.borrow();
+ for t in generics.iter() {
+ if let Some(t) = t {
+ translated_fn.add_generic_type(t.clone());
+ }
+ }
+
+ let mut t = Self {
env,
proc,
info,
@@ -376,10 +655,20 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
procedure_registry: proc_registry,
attrs,
ty_translator,
- inputs,
- output,
const_registry,
};
+ // add universal constraints
+ let universal_constraints = t.get_relevant_universal_constraints();
+ info!("univeral constraints: {:?}", universal_constraints);
+ for (lft1, lft2) in universal_constraints.into_iter() {
+ t.translated_fn
+ .add_universal_lifetime_constraint(lft1, lft2)
+ .map_err(|e| TranslationError::UnknownError(e))?;
+ }
+
+ // process attributes
+ t.process_attrs(inputs.as_slice(), &output)?;
+
Ok(t)
},
Err(err) => Err(TranslationError::UnknownError(format!("{:?}", err))),
@@ -416,22 +705,70 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
if uk2 == info::UniversalRegionKind::Function {
continue;
}
+
+ let to_universal = || {
+ let x = self.to_universal_lft(uk1, *r2)?;
+ let y = self.to_universal_lft(uk2, *r1)?;
+ Some((x, y))
+ };
// else, add this constraint
// for the purpose of this analysis, it is fine to treat it as a dynamic inclusion
- self.inclusion_tracker.add_dynamic_inclusion(*r1, *r2, root_point);
- universal_constraints
- .push((self.to_universal_lft(uk1, *r2), self.to_universal_lft(uk2, *r1)));
+ if let Some((x, y)) = to_universal() {
+ self.inclusion_tracker.add_dynamic_inclusion(*r1, *r2, root_point);
+ universal_constraints.push((x, y));
+ };
}
}
}
universal_constraints
}
+ /// Parse and process attributes of this closure.
+ fn process_closure_attrs<'b>(
+ &mut self,
+ inputs: &[Ty<'tcx>],
+ output: &Ty<'tcx>,
+ meta: ClosureMetaInfo<'b, 'tcx, 'def>,
+ ) -> Result<(), TranslationError> {
+ trace!("entering process_closure_attrs");
+ let v = self.attrs;
+
+ info!("inputs: {:?}, output: {:?}", inputs, output);
+ let mut translated_arg_types: Vec<radium::Type<'def>> = Vec::new();
+ let generic_env = &*self.ty_translator.generic_scope.borrow();
+ for arg in inputs.iter() {
+ let mut translated: radium::Type<'def> = self.ty_translator.translate_type(arg)?;
+ translated.subst_params(generic_env.as_slice());
+ translated_arg_types.push(translated);
+ }
+ let mut translated_ret_type: radium::Type<'def> = self.ty_translator.translate_type(output)?;
+ translated_ret_type.subst_params(generic_env.as_slice());
+ info!("translated function type: {:?} → {}", translated_arg_types, translated_ret_type);
+
+ let parser = rrconfig::attribute_parser();
+ match parser.as_str() {
+ "verbose" => {
+ let ty_translator = &self.ty_translator;
+ let mut parser: VerboseFunctionSpecParser<'_, 'def, _> =
+ VerboseFunctionSpecParser::new(&translated_arg_types, &translated_ret_type, |lit| {
+ ty_translator.intern_literal(lit)
+ });
+ parser
+ .parse_closure_spec(v, &mut self.translated_fn, meta, |x| ty_translator.make_tuple_use(x))
+ .map_err(|e| TranslationError::AttributeError(e))?;
+ trace!("leaving process_closure_attrs");
+ Ok(())
+ },
+ _ => {
+ trace!("leaving process_closure_attrs");
+ Err(TranslationError::UnknownAttributeParser(parser))
+ },
+ }
+ }
+
/// Parse and process attributes of this function.
- fn process_attrs(&mut self) -> Result<(), TranslationError> {
+ fn process_attrs(&mut self, inputs: &[Ty<'tcx>], output: &Ty<'tcx>) -> Result<(), TranslationError> {
let v = self.attrs;
- let inputs = &self.inputs;
- let output = &self.output;
info!("inputs: {:?}, output: {:?}", inputs, output);
let mut translated_arg_types: Vec<radium::Type<'def>> = Vec::new();
@@ -463,45 +800,33 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
}
// TODO refactor/ move
- fn to_universal_lft(&self, k: info::UniversalRegionKind, r: Region) -> radium::UniversalLft {
+ fn to_universal_lft(&self, k: info::UniversalRegionKind, r: Region) -> Option<radium::UniversalLft> {
match k {
- info::UniversalRegionKind::Function => radium::UniversalLft::Function,
- info::UniversalRegionKind::Static => radium::UniversalLft::Static,
+ info::UniversalRegionKind::Function => Some(radium::UniversalLft::Function),
+ info::UniversalRegionKind::Static => Some(radium::UniversalLft::Static),
info::UniversalRegionKind::Local => {
- radium::UniversalLft::Local(self.ty_translator.lookup_universal_lifetime(r).unwrap())
+ self.ty_translator.lookup_universal_region(r).map(|x| radium::UniversalLft::Local(x))
},
info::UniversalRegionKind::External => {
- radium::UniversalLft::External(self.ty_translator.lookup_universal_lifetime(r).unwrap())
+ self.ty_translator.lookup_universal_region(r).map(|x| radium::UniversalLft::External(x))
},
}
}
/// Translation that only generates a specification.
pub fn generate_spec(mut self) -> Result<radium::FunctionSpec<'def>, TranslationError> {
- // add universal constraints
- let universal_constraints = self.get_relevant_universal_constraints();
- info!("univeral constraints: {:?}", universal_constraints);
- for (lft1, lft2) in universal_constraints.into_iter() {
- self.translated_fn
- .add_universal_lifetime_constraint(lft1, lft2)
- .map_err(|e| TranslationError::UnknownError(e))?;
- }
-
- // process attributes
- self.process_attrs()?;
-
self.ty_translator.leave_procedure();
Ok(self.translated_fn.into())
}
/// Generate a string identifier for a Local.
- /// Tries to find the Rust source code name of the local,
- /// otherwise simply enumerates.
- /// This function is deterministic, so subsequent calls with the same `Local` will always
- /// generate the same name.
- fn make_local_name(mir_body: &Body<'tcx>, local: &Local) -> String {
- if let Some(mir_name) = Self::find_name_for_local(mir_body, local) {
- strip_coq_ident(&mir_name)
+ /// Tries to find the Rust source code name of the local, otherwise simply enumerates.
+ /// `used_names` keeps track of the Rust source code names that have already been used.
+ fn make_local_name(mir_body: &Body<'tcx>, local: &Local, used_names: &mut HashSet<String>) -> String {
+ if let Some(mir_name) = Self::find_name_for_local(mir_body, local, &used_names) {
+ let name = strip_coq_ident(&mir_name);
+ used_names.insert(mir_name);
+ name
} else {
let mut name = "__".to_string();
name.push_str(&local.index().to_string());
@@ -510,16 +835,29 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
}
/// Find a source name for a local of a MIR body, if possible.
- fn find_name_for_local(body: &mir::Body<'tcx>, local: &mir::Local) -> Option<String> {
+ fn find_name_for_local(
+ body: &mir::Body<'tcx>,
+ local: &mir::Local,
+ used_names: &HashSet<String>,
+ ) -> Option<String> {
let debug_info = &body.var_debug_info;
for dbg in debug_info {
let name = &dbg.name;
let val = &dbg.value;
match *val {
VarDebugInfoContents::Place(l) => {
- // TODO: make sure that l.projection is empty?
- if l.local == *local {
- return Some(name.as_str().to_string());
+ // make sure that the place projection is empty -- otherwise this might just
+ // refer to the capture of a closure
+ if let Some(this_local) = l.as_local() {
+ if this_local == *local {
+ // around closures, multiple symbols may be mapped to the same name.
+ // To prevent this from happening, we check that the name hasn't been
+ // used already
+ // TODO: find better solution
+ if !used_names.contains(name.as_str()) {
+ return Some(name.as_str().to_string());
+ }
+ }
}
},
VarDebugInfoContents::Const(_) => {
@@ -531,19 +869,26 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
return None;
}
- pub fn translate(mut self) -> Result<radium::Function<'def>, TranslationError> {
- // add universal constraints
- let universal_constraints = self.get_relevant_universal_constraints();
- info!("univeral constraints: {:?}", universal_constraints);
- for (lft1, lft2) in universal_constraints.into_iter() {
- self.translated_fn
- .add_universal_lifetime_constraint(lft1, lft2)
- .map_err(|e| TranslationError::UnknownError(e))?;
+ fn dump_body(body: &Body) {
+ // TODO: print to file
+ let basic_blocks = &body.basic_blocks;
+ for (bb_idx, bb) in basic_blocks.iter_enumerated() {
+ Self::dump_basic_block(&bb_idx, bb);
}
+ }
- // process attributes
- self.process_attrs()?;
+ /// Dump a basic block as info debug output.
+ fn dump_basic_block(bb_idx: &BasicBlock, bb: &BasicBlockData) {
+ info!("Basic block {:?}:", bb_idx);
+ let mut i = 0;
+ for s in &bb.statements {
+ info!("{}\t{:?}", i, s);
+ i += 1;
+ }
+ info!("{}\t{:?}", i, bb.terminator());
+ }
+ pub fn translate(mut self) -> Result<radium::Function<'def>, TranslationError> {
let body = self.proc.get_mir();
// analyze which locals are used for the result of checked-ops, because we will
@@ -558,10 +903,14 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
let local_decls = &body.local_decls;
info!("Have {} local decls\n", local_decls.len());
+ let debug_info = &body.var_debug_info;
+ info!("using debug info: {:?}", debug_info);
+
let mut return_synty = radium::SynType::Unit; // default
let mut fn_locals = Vec::new();
let mut opt_return_name =
Err(TranslationError::UnknownError("could not find local for return value".to_string()));
+ let mut used_names = HashSet::new();
// go over local_decls and create the right radium:: stack layout
for (local, local_decl) in local_decls.iter_enumerated() {
let kind = body.local_kind(local);
@@ -586,7 +935,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
tr_ty.subst_params(&self.ty_translator.generic_scope.borrow());
let st = tr_ty.get_syn_type();
- let name = Self::make_local_name(body, &local);
+ let name = Self::make_local_name(body, &local, &mut used_names);
radium_name_map.insert(local, name.to_string());
fn_locals.push((local, name.clone(), tr_ty));
@@ -602,6 +951,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
},
}
}
+ info!("radium name map: {:?}", radium_name_map);
// create the function
let return_name = opt_return_name?;
@@ -623,8 +973,6 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
ty_translator: self.ty_translator,
loop_specs: HashMap::new(),
fn_locals,
- inputs: self.inputs,
- output: self.output,
checked_op_temporaries: checked_op_locals,
const_registry: self.const_registry,
collected_statics: HashSet::new(),
@@ -686,12 +1034,6 @@ struct BodyTranslator<'a, 'def, 'tcx> {
/// relevant locals: (local, name, type)
fn_locals: Vec<(Local, String, radium::Type<'def>)>,
- /// inputs of the function, with both early and late bound regions substituted with their
- /// Polonius ReVar
- inputs: Vec<Ty<'tcx>>,
- /// output of the function, similarly with substituted regions
- output: Ty<'tcx>,
-
/// result temporaries of checked ops that we rewrite
/// we assume that this place is typed at (result_type, bool)
/// and rewrite accesses to the first component to directly use the place,
@@ -706,8 +1048,6 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
/// if successful.
pub fn translate(mut self) -> Result<radium::Function<'def>, TranslationError> {
let body = self.proc.get_mir();
- // dump debug info
- Self::dump_body(body);
// add lifetime parameters to the map
let initial_constraints = self.get_initial_universal_arg_constraints();
@@ -867,11 +1207,13 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
did: &DefId,
ty_params: ty::GenericArgsRef<'tcx>,
) -> Result<String, TranslationError> {
+ trace!("enter register_use_procedure did={:?} ty_params={:?}", did, ty_params);
let key = self.generate_procedure_inst_key(ty_params)?;
let tup = (*did, key);
+ let res;
if let Some((n, ..)) = self.collected_procedures.get(&tup) {
- Ok(format!("{}", n))
+ res = format!("{}", n);
} else {
// lookup the name in the procedure registry
@@ -889,6 +1231,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
let generic_env = &*self.ty_translator.generic_scope.borrow();
// TODO: maybe come up with some better way to generate names
+ info!("register_use_procedure: translating args {:?}", tup.1);
for p in tup.1.iter() {
mangled_name.push_str(format!("_{}", p).as_str());
@@ -903,10 +1246,41 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
// also gather all the layouts of the arguments.
let full_ty: ty::EarlyBinder<Ty<'tcx>> = self.env.tcx().type_of(*did);
let full_ty: Ty<'tcx> = full_ty.instantiate_identity();
- let sig = full_ty.fn_sig(self.env.tcx());
- let inputs = sig.inputs().skip_binder();
+ let mut inputs = Vec::new();
let mut syntypes = Vec::new();
+ match full_ty.kind() {
+ ty::TyKind::FnDef(_, _) => {
+ let sig = full_ty.fn_sig(self.env.tcx());
+ for ty in sig.inputs().skip_binder().iter() {
+ inputs.push(*ty);
+ }
+ },
+ ty::TyKind::Closure(_, args) => {
+ let clos_args = args.as_closure();
+ let pre_sig = clos_args.sig().skip_binder();
+ // we also need to add the closure argument here
+ // in this case, we need to patch the region first
+
+ let tuple_ty = clos_args.tupled_upvars_ty();
+ match clos_args.kind() {
+ ty::ClosureKind::Fn => {
+ syntypes.push(radium::SynType::Ptr);
+ },
+ ty::ClosureKind::FnMut => {
+ syntypes.push(radium::SynType::Ptr);
+ },
+ ty::ClosureKind::FnOnce => {
+ inputs.push(tuple_ty);
+ },
+ }
+ for ty in pre_sig.inputs().iter() {
+ inputs.push(*ty);
+ }
+ },
+ _ => unimplemented!(),
+ }
+
//info!("substs: {:?}, inputs {:?} ", ty_params, inputs);
for i in inputs.iter() {
// need to wrap it, because there's no Subst instance for Ty
@@ -923,16 +1297,10 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
);
self.collected_procedures
.insert(tup, (loc_name.clone(), spec_name.to_string(), translated_params, syntypes));
- Ok(loc_name)
- }
- }
-
- fn dump_body(body: &Body) {
- // TODO: print to file
- let basic_blocks = &body.basic_blocks;
- for (bb_idx, bb) in basic_blocks.iter_enumerated() {
- Self::dump_basic_block(&bb_idx, bb);
+ res = loc_name;
}
+ trace!("leave register_use_procedure");
+ Ok(res)
}
fn compute_regions_of_function(tcx: ty::TyCtxt<'tcx>, did: DefId) {
@@ -1024,17 +1392,6 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
// Then try to fix issue with stuff
}
- /// Dump a basic block as info debug output.
- fn dump_basic_block(bb_idx: &BasicBlock, bb: &BasicBlockData) {
- info!("Basic block {:?}:", bb_idx);
- let mut i = 0;
- for s in &bb.statements {
- info!("{}\t{:?}", i, s);
- i += 1;
- }
- info!("{}\t{:?}", i, bb.terminator());
- }
-
/// Enqueues a basic block for processing, if it has not already been processed,
/// and marks it as having been processed.
fn enqueue_basic_block(&mut self, bb: BasicBlock) {
@@ -1051,7 +1408,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
info::AtomicRegion::Loan(_, r) => {
format!("llft{}", r.index())
},
- info::AtomicRegion::Universal(_, r) => match self.ty_translator.lookup_universal_lifetime(*r) {
+ info::AtomicRegion::Universal(_, r) => match self.ty_translator.lookup_universal_region(*r) {
Some(s) => s,
None => format!("ulft{}", r.index()),
},
@@ -1179,12 +1536,12 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
_rhs_ty: Ty<'tcx>,
strong_update: bool,
loc: Location,
- ) -> Vec<(Region, Region, PointIndex)> {
+ ) -> HashSet<(Region, Region, PointIndex)> {
let info = &self.info;
let input_facts = &info.borrowck_in_facts;
let subset_base = &input_facts.subset_base;
- let mut constraints = Vec::new();
+ let mut constraints = HashSet::new();
// Polonius subset constraint are spawned for the midpoint
let midpoint = self.info.interner.get_point_index(&facts::Point {
location: loc,
@@ -1197,8 +1554,8 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
for (s1, s2, point) in subset_base.iter() {
if *point == midpoint {
// take this constraint and the reverse constraint
- constraints.push((*s1, *s2, *point));
- constraints.push((*s2, *s1, *point));
+ constraints.insert((*s1, *s2, *point));
+ constraints.insert((*s2, *s1, *point));
}
}
} else {
@@ -1211,7 +1568,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
if !self.inclusion_tracker.check_inclusion(*s1, *s2, *point) {
// only add it if it does not hold already, since we will enforce this
// constraint dynamically.
- constraints.push((*s1, *s2, *point));
+ constraints.insert((*s1, *s2, *point));
}
}
}
@@ -1220,52 +1577,6 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
constraints
}
- /// Generate a dynamic inclusion of r1 in r2 at point p. Prepends annotations for doing so to `cont`.
- fn generate_dyn_inclusion(
- &mut self,
- r1: Region,
- r2: Region,
- p: PointIndex,
- cont: radium::Stmt,
- ) -> radium::Stmt {
- // check if inclusion already holds
- if self.inclusion_tracker.check_inclusion(r1, r2, p) {
- // inclusion already holds, done
- cont
- } else {
- // check if the reverse inclusion already holds
- if self.inclusion_tracker.check_inclusion(r2, r1, p) {
- // our invariant is that this must be a static inclusion
- assert!(self.inclusion_tracker.check_static_inclusion(r2, r1, p));
-
- self.inclusion_tracker.add_dynamic_inclusion(r1, r2, p);
-
- // we generate an extendlft instruction
- // for this, we need to figure out a path to make this inclusion true, i.e. we need
- // an explanation of why it is syntactically included.
- // TODO: for now, we just assume that r1 ⊑ₗ [r2] (in terms of Coq lifetime inclusion)
- radium::Stmt::Annot {
- a: radium::Annotation::ExtendLft(
- self.format_atomic_region(&info::AtomicRegion::PlaceRegion(r1)),
- ),
- s: Box::new(cont),
- }
- } else {
- self.inclusion_tracker.add_dynamic_inclusion(r1, r2, p);
- // we generate a dynamic inclusion instruction
- // we flip this around because the annotations are talking about lifetimes, which are oriented
- // the other way around.
- radium::Stmt::Annot {
- a: radium::Annotation::DynIncludeLft(
- self.format_atomic_region(&info::AtomicRegion::PlaceRegion(r2)),
- self.format_atomic_region(&info::AtomicRegion::PlaceRegion(r1)),
- ),
- s: Box::new(cont),
- }
- }
- }
- }
-
/// Split the type of a function operand of a call expression to a base type and an instantiation for
/// generics.
fn call_expr_op_split_inst(
@@ -1459,6 +1770,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
ref target,
..
} => {
+ trace!("translating Call {:?}", term);
let is_panic = self.is_call_destination_panic(func)?;
if is_panic {
info!("Replacing call to std::panicking::begin_panic with Stuck");
@@ -2026,6 +2338,71 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
}
}
+ /// Generate a dynamic inclusion of r1 in r2 at point p. Prepends annotations for doing so to `cont`.
+ fn generate_dyn_inclusion(
+ &mut self,
+ r1: Region,
+ r2: Region,
+ p: PointIndex,
+ cont: radium::Stmt,
+ ) -> radium::Stmt {
+ // check if inclusion already holds
+ if self.inclusion_tracker.check_inclusion(r1, r2, p) {
+ // inclusion already holds, done
+ cont
+ } else {
+ // check if the reverse inclusion already holds
+ if self.inclusion_tracker.check_inclusion(r2, r1, p) {
+ // our invariant is that this must be a static inclusion
+ assert!(self.inclusion_tracker.check_static_inclusion(r2, r1, p));
+ self.inclusion_tracker.add_dynamic_inclusion(r1, r2, p);
+
+ // we generate an extendlft instruction
+ // for this, we need to figure out a path to make this inclusion true, i.e. we need
+ // an explanation of why it is syntactically included.
+ // TODO: for now, we just assume that r1 ⊑ₗ [r2] (in terms of Coq lifetime inclusion)
+ radium::Stmt::Annot {
+ a: radium::Annotation::ExtendLft(
+ self.format_atomic_region(&info::AtomicRegion::PlaceRegion(r1)),
+ ),
+ s: Box::new(cont),
+ }
+ } else {
+ self.inclusion_tracker.add_dynamic_inclusion(r1, r2, p);
+ // we generate a dynamic inclusion instruction
+ // we flip this around because the annotations are talking about lifetimes, which are oriented
+ // the other way around.
+ radium::Stmt::Annot {
+ a: radium::Annotation::DynIncludeLft(
+ self.format_atomic_region(&info::AtomicRegion::PlaceRegion(r2)),
+ self.format_atomic_region(&info::AtomicRegion::PlaceRegion(r1)),
+ ),
+ s: Box::new(cont),
+ }
+ }
+ }
+ }
+
+ /// Generates dynamic inclusions for the set of inclusions in `incls`.
+ /// These inclusions should not hold yet.
+ /// Skips mutual inclusions -- we cannot interpret these.
+ fn generate_dyn_inclusions(
+ &mut self,
+ incls: HashSet<(Region, Region, PointIndex)>,
+ mut cont_stmt: radium::Stmt,
+ ) -> radium::Stmt {
+ // before executing the assignment, first enforce dynamic inclusions
+ info!("Generating dynamic inclusions {:?}", incls);
+ for (r1, r2, p) in incls.iter() {
+ if !incls.contains(&(*r2, *r1, *p)) {
+ cont_stmt = self.generate_dyn_inclusion(*r1, *r2, *p, cont_stmt);
+ } else {
+ warn!("Skipping impossible dynamic inclusion {:?} ⊑ {:?} at {:?}", r1, r2, p);
+ }
+ }
+ cont_stmt
+ }
+
/**
* Translate a single basic block.
*/
@@ -2078,11 +2455,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
dying_loans.insert(*l);
}
}
- cont_stmt = self.prepend_endlfts(cont_stmt, dying_loans.into_iter());
-
- //let dying = self.info.get_dying_loans(loc);
- //let dying_zombie = self.info.get_dying_zombie_loans(loc);
- //cont_stmt = self.prepend_endlfts(cont_stmt, dying_zombie);
+ // we prepend them before the current statement
// check for attributes on this statement
let scopes = &self.proc.get_mir().source_scopes;
@@ -2107,6 +2480,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
// if this is a checked op, be sure to remember it
if let Some(rewritten_ty) = self.checked_op_temporaries.get(&plc.local) {
+ info!("rewriting assignment to checked op: {:?}", plc);
// this should be a temporary
assert!(plc.projection.is_empty());
@@ -2156,7 +2530,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
// similarly generate an annotation that encodes these constraints in the RR
// type system
translated_val = self.generate_strong_update_annot(plc_ty, translated_val);
- new_dyn_inclusions = Vec::new();
+ new_dyn_inclusions = HashSet::new();
} else {
// need to filter out the constraints that are relevant here.
// incrementally go through them.
@@ -2261,10 +2635,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
}
}
- // before executing the assignment, first enforce dynamic inclusions
- for (r1, r2, p) in new_dyn_inclusions.iter() {
- cont_stmt = self.generate_dyn_inclusion(*r1, *r2, *p, cont_stmt);
- }
+ cont_stmt = self.generate_dyn_inclusions(new_dyn_inclusions, cont_stmt);
}
}
},
@@ -2336,6 +2707,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
()
},
}
+ cont_stmt = self.prepend_endlfts(cont_stmt, dying_loans.into_iter());
}
Ok(cont_stmt)
@@ -2721,6 +3093,29 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
});
}
},
+ box mir::AggregateKind::Closure(def, args) => {
+ trace!("Translating Closure aggregate value for {:?}", def);
+ // We basically translate this to a tuple
+ if operand_types.len() == 0 {
+ // translate to unit literal
+ Ok(radium::Expr::Literal(radium::Literal::LitZST))
+ } else {
+ let struct_use = self.ty_translator.generate_tuple_use(
+ operand_types.iter().map(|r| *r),
+ TranslationState::InFunction,
+ )?;
+ let sl = struct_use.generate_raw_syn_type_term();
+ let initializers: Vec<_> = translated_ops
+ .into_iter()
+ .enumerate()
+ .map(|(i, o)| (i.to_string(), o))
+ .collect();
+ Ok(radium::Expr::StructInitE {
+ sls: radium::CoqAppTerm::new_lhs(sl.to_string()),
+ components: initializers,
+ })
+ }
+ },
_ => {
// TODO
Err(TranslationError::UnsupportedFeature {
@@ -2904,9 +3299,47 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
fn translate_fn_def_use(&mut self, ty: Ty<'tcx>) -> Result<radium::Expr, TranslationError> {
match ty.kind() {
TyKind::FnDef(defid, params) => {
- // track that we are using this function and generate the Coq location name
- let param_name = self.register_use_procedure(defid, params)?;
- Ok(radium::Expr::MetaParam(param_name))
+ let key: ty::ParamEnv<'tcx> = self.env.tcx().param_env(self.proc.get_id());
+ if self.env.tcx().trait_of_item(*defid).is_some() {
+ if let Some((resolved_did, resolved_params, kind)) =
+ crate::traits::resolve_assoc_item(self.env.tcx(), key, *defid, params)
+ {
+ info!(
+ "Resolved trait method {:?} as {:?} with substs {:?} and kind {:?}",
+ defid, resolved_did, resolved_params, kind
+ );
+ match kind {
+ crate::traits::TraitResolutionKind::UserDefined => {
+ let param_name =
+ self.register_use_procedure(&resolved_did, resolved_params)?;
+ Ok(radium::Expr::MetaParam(param_name))
+ },
+ crate::traits::TraitResolutionKind::Param => {
+ Err(TranslationError::Unimplemented {
+ description: format!("Implement trait invocation for Param"),
+ })
+ },
+ crate::traits::TraitResolutionKind::Closure => {
+ // TODO: here, we should first generate an instance of the trait
+ //self.env.tcx().
+ // mir_shims(rustc_middle::ty::InstanceDef::Item(resolved_did));
+ // the args are just the closure args. We can ignore them.
+ let _clos_args = resolved_params.as_closure();
+ let param_name =
+ self.register_use_procedure(&resolved_did, ty::List::empty())?;
+ Ok(radium::Expr::MetaParam(param_name))
+ //Err(TranslationError::Unimplemented { description: format!("Implement trait
+ // invocation for Closure") })
+ },
+ }
+ } else {
+ Err(TranslationError::TraitResolution(format!("Could not resolve trait {:?}", defid)))
+ }
+ } else {
+ // track that we are using this function and generate the Coq location name
+ let param_name = self.register_use_procedure(defid, params)?;
+ Ok(radium::Expr::MetaParam(param_name))
+ }
},
_ => Err(TranslationError::UnknownError("not a FnDef type".to_string())),
}
@@ -3171,6 +3604,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
// update cur_ty
cur_ty = cur_ty.projection_ty(self.env.tcx(), *it);
}
+ info!("translating place {:?} to {:?}", pl, acc_expr);
Ok(acc_expr)
}
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index e0d6e99495b8c7740ae95f9187b9556c4e09b996..2e2fbc6d28561df671590b803db2b025387ccd17 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -18,6 +18,7 @@ extern crate rustc_driver;
extern crate rustc_errors;
extern crate rustc_hir;
extern crate rustc_index;
+extern crate rustc_infer;
extern crate rustc_interface;
extern crate rustc_middle;
extern crate rustc_session;
@@ -49,6 +50,7 @@ mod function_body;
mod inclusion_tracker;
mod shim_registry;
mod spec_parsers;
+mod traits;
mod type_translator;
mod tyvars;
mod utils;
@@ -60,14 +62,13 @@ use crate_parser::CrateAttrParser;
use environment::Environment;
use function_body::{ConstScope, FunctionTranslator, ProcedureMode, ProcedureScope};
use mod_parser::ModuleAttrParser;
-use parse::{MToken, Parse, ParseResult, ParseStream, Peek};
+use rrconfig;
use spec_parsers::verbose_function_spec_parser::{get_export_as_attr, get_shim_attrs};
use spec_parsers::{
const_attr_parser as const_parser, crate_attr_parser as crate_parser, module_attr_parser as mod_parser,
};
use topological_sort::TopologicalSort;
use type_translator::TypeTranslator;
-use {attribute_parse as parse, rrconfig};
/// Order ADT definitions topologically.
fn order_adt_defs<'tcx>(deps: HashMap<DefId, HashSet<DefId>>) -> Vec<DefId> {
@@ -856,17 +857,40 @@ fn translate_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) {
continue;
}
- info!("Translating function {}", fname);
-
- let translator = FunctionTranslator::new(
- &vcx.env,
- meta,
- proc,
- &filtered_attrs,
- &vcx.type_translator,
- &vcx.procedure_registry,
- &vcx.const_registry,
- );
+ info!("\nTranslating function {}", fname);
+
+ let translator;
+
+ let ty: ty::EarlyBinder<ty::Ty<'tcx>> = vcx.env.tcx().type_of(proc.get_id());
+ let ty = ty.instantiate_identity();
+ match ty.kind() {
+ ty::TyKind::FnDef(_def, _args) => {
+ translator = FunctionTranslator::new(
+ &vcx.env,
+ meta,
+ proc,
+ &filtered_attrs,
+ &vcx.type_translator,
+ &vcx.procedure_registry,
+ &vcx.const_registry,
+ )
+ },
+ ty::TyKind::Closure(_, _) => {
+ translator = FunctionTranslator::new_closure(
+ &vcx.env,
+ meta,
+ proc,
+ &filtered_attrs,
+ &vcx.type_translator,
+ &vcx.procedure_registry,
+ &vcx.const_registry,
+ )
+ },
+ _ => {
+ translator =
+ Err(function_body::TranslationError::UnknownError("unknown function kind".to_string()));
+ },
+ };
if mode.is_only_spec() {
// Only generate a spec
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 7ef8d081bdd4ebeb958f3fae729b73b2761eb06c..11da0c8c4ceadd63017cb302b904144df997f322 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
@@ -4,14 +4,30 @@
// If a copy of the BSD-3-clause license was not distributed with this
// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
-use log::{debug, info};
+use std::collections::HashMap;
+use std::fmt::Write;
+
+use log::{debug, info, warn};
use parse::{MToken, Parse, ParseResult, ParseStream, Peek};
use radium::specs;
use rustc_ast::ast::AttrItem;
+use rustc_middle::ty;
use {attribute_parse as parse, radium};
use crate::spec_parsers::parse_utils::{ParseMeta, *};
+pub struct ClosureMetaInfo<'a, 'tcx, 'def> {
+ /// the closure kind
+ pub kind: ty::ClosureKind,
+ /// capture information
+ pub captures: &'tcx [&'tcx ty::CapturedPlace<'tcx>],
+ /// the translated types of the captures, including the surrounding reference if captured by-ref.
+ /// Needs to be in same order as `captures`
+ pub capture_tys: &'a [specs::Type<'def>],
+ /// the lifetime of the closure, if kind is `Fn` or `FnMut`
+ pub closure_lifetime: Option<specs::Lft>,
+}
+
pub trait FunctionSpecParser<'def> {
/// Parse a set of attributes into a function spec.
/// The implementation can assume the `attrs` to be prefixed by the tool prefix (e.g. `rr`) and
@@ -21,6 +37,19 @@ pub trait FunctionSpecParser<'def> {
attrs: &'a [&'a AttrItem],
spec: &'a mut radium::FunctionBuilder<'def>,
) -> Result<(), String>;
+
+ /// Parse a set of attributes into a closure spec.
+ /// The implementation can assume the `attrs` to be prefixed by the tool prefix (e.g. `rr`) and
+ /// that it does not need to deal with any other attributes.
+ fn parse_closure_spec<'tcx, 'a, 'c, F>(
+ &'a mut self,
+ attrs: &'a [&'a AttrItem],
+ spec: &'a mut radium::FunctionBuilder<'def>,
+ meta: ClosureMetaInfo<'c, 'tcx, 'def>,
+ make_tuple: F,
+ ) -> Result<(), String>
+ where
+ F: Fn(Vec<specs::Type<'def>>) -> specs::Type<'def>;
}
/// A sequence of refinements with optional types, e.g.
@@ -39,6 +68,50 @@ impl<'a> Parse<ParseMeta<'a>> for RRArgs {
}
}
+/// Representation of the spec for a single closure capture.
+/// e.g. `"x" : "#42"` (for by shr-ref capture)
+/// or `"y" : "(#42, γ)" -> "(#43, γ)"` (for by mut-ref capture)
+struct ClosureCaptureSpec {
+ variable: String,
+ pre: LiteralTypeWithRef,
+ post: Option<LiteralTypeWithRef>,
+}
+
+impl<'a> parse::Parse<ParseMeta<'a>> for ClosureCaptureSpec {
+ fn parse(input: parse::ParseStream, meta: &ParseMeta) -> parse::ParseResult<Self> {
+ let name_str: parse::LitStr = input.parse(meta)?;
+ let name = name_str.value();
+ input.parse::<_, parse::MToken![:]>(meta)?;
+
+ let pre_spec: LiteralTypeWithRef = input.parse(meta)?;
+
+ if parse::RArrow::peek(input) {
+ input.parse::<_, parse::MToken![->]>(meta)?;
+ let current_pos = input.pos().unwrap();
+
+ let post_spec: LiteralTypeWithRef = input.parse(meta)?;
+ if post_spec.ty.is_some() {
+ Err(parse::ParseError::OtherErr(
+ current_pos,
+ format!("Did not expect type specification for capture postcondition"),
+ ))
+ } else {
+ Ok(ClosureCaptureSpec {
+ variable: name,
+ pre: pre_spec,
+ post: Some(post_spec),
+ })
+ }
+ } else {
+ Ok(ClosureCaptureSpec {
+ variable: name,
+ pre: pre_spec,
+ post: None,
+ })
+ }
+ }
+}
+
/// Representation of the IProps that can appear in a requires or ensures clause.
enum MetaIProp {
/// #[rr::requires("..")] or #[rr::requires("Ha" : "..")]
@@ -201,10 +274,390 @@ fn str_err(e: parse::ParseError) -> String {
format!("{:?}", e)
}
+impl<'a, 'def, F> VerboseFunctionSpecParser<'a, 'def, F>
+where
+ F: Fn(specs::LiteralType) -> specs::LiteralTypeRef<'def>,
+{
+ /// Handles attributes common among functions/methods and closures.
+ fn handle_common_attributes(
+ &mut self,
+ name: &str,
+ buffer: &parse::ParseBuffer,
+ builder: &mut radium::FunctionBuilder<'def>,
+ lfts: &[(Option<String>, String)],
+ ) -> Result<bool, String> {
+ let meta: &[specs::LiteralTyParam] = builder.get_ty_params();
+ let meta: ParseMeta = (&meta, lfts);
+
+ match name {
+ "params" => {
+ let params = RRParams::parse(&buffer, &meta).map_err(str_err)?;
+ for p in params.params {
+ builder.spec.add_param(p.name, p.ty)?;
+ }
+ },
+ "param" => {
+ let param = RRParam::parse(&buffer, &meta).map_err(str_err)?;
+ builder.spec.add_param(param.name, param.ty)?;
+ },
+ "args" => {
+ let args = RRArgs::parse(&buffer, &meta).map_err(str_err)?;
+ if self.arg_types.len() != args.args.len() {
+ return Err(format!(
+ "wrong number of function arguments given: expected {} args",
+ self.arg_types.len()
+ ));
+ }
+ for (arg, ty) in args.args.into_iter().zip(self.arg_types) {
+ let (ty, hint) = self.make_type_with_ref(&arg, ty);
+ builder.spec.add_arg(ty)?;
+ if let Some(cty) = hint {
+ // potentially add a typing hint to the refinement
+ if let IdentOrTerm::Ident(ref i) = arg.rfn {
+ info!("Trying to add a typing hint for {}", i);
+ builder.spec.add_param_type_annot(&specs::CoqName::Named(i.clone()), cty)?;
+ }
+ }
+ }
+ },
+ "requires" => {
+ let iprop = MetaIProp::parse(&buffer, &meta).map_err(str_err)?;
+ builder.spec.add_precondition(iprop.into())?;
+ },
+ "ensures" => {
+ let iprop = MetaIProp::parse(&buffer, &meta).map_err(str_err)?;
+ builder.spec.add_postcondition(iprop.into())?;
+ },
+ "observe" => {
+ let m = || {
+ let gname: parse::LitStr = buffer.parse(&meta)?;
+ buffer.parse::<_, parse::MToken![:]>(&meta)?;
+
+ let term: parse::LitStr = buffer.parse(&meta)?;
+ let (term, _) = process_coq_literal(&term.value(), meta);
+ Ok(MetaIProp::Observe(gname.value().to_string(), term))
+ };
+ let m = m().map_err(str_err)?;
+ builder.spec.add_postcondition(m.into())?;
+ },
+ "returns" => {
+ let tr = LiteralTypeWithRef::parse(&buffer, &meta).map_err(str_err)?;
+ // convert to type
+ let (ty, _) = self.make_type_with_ref(&tr, self.ret_type);
+ builder.spec.set_ret_type(ty)?;
+ },
+ "exists" => {
+ let params = RRParams::parse(&buffer, &meta).map_err(str_err)?;
+ for param in params.params.into_iter() {
+ builder.spec.add_existential(param.name, param.ty)?;
+ }
+ },
+ "tactics" => {
+ let tacs = parse::LitStr::parse(&buffer, &meta).map_err(str_err)?;
+ let tacs = tacs.value();
+ builder.add_manual_tactic(&tacs);
+ },
+ "context" => {
+ let context_item = RRCoqContextItem::parse(&buffer, &meta).map_err(str_err)?;
+ if context_item.at_end {
+ builder.spec.add_late_coq_param(
+ specs::CoqName::Unnamed,
+ specs::CoqType::Literal(context_item.item),
+ true,
+ )?;
+ } else {
+ builder.spec.add_coq_param(
+ specs::CoqName::Unnamed,
+ specs::CoqType::Literal(context_item.item),
+ true,
+ )?;
+ }
+ },
+ _ => {
+ return Ok(false);
+ },
+ }
+ Ok(true)
+ }
+
+ /// Merges information on captured variables with specifications on captures.
+ /// `capture_specs`: the parsed capture specification
+
+ /// `make_tuple`: closure to make a new Radium tuple type
+ /// `builder`: the function builder to push new specification components to
+ fn merge_capture_information<'b, 'c, 'tcx, H>(
+ &mut self,
+ capture_specs: Vec<ClosureCaptureSpec>,
+ meta: ClosureMetaInfo<'c, 'tcx, 'def>,
+ make_tuple: H,
+ builder: &mut radium::FunctionBuilder<'def>,
+ ) -> Result<(), String>
+ where
+ H: Fn(Vec<specs::Type<'def>>) -> specs::Type<'def>,
+ {
+ enum CapturePostRfn {
+ // mutable capture: (pattern, ghost_var)
+ Mut(String, String),
+ // immutable or once capture: pattern
+ ImmutOrConsume(String),
+ }
+
+ // new ghost vars created for mut-captures
+ let mut new_ghost_vars: Vec<String> = Vec::new();
+ let mut pre_types: Vec<specs::TypeWithRef> = Vec::new();
+ // post patterns and optional ghost variable, if this is a by-mut-ref capture
+ let mut post_patterns: Vec<CapturePostRfn> = Vec::new();
+
+ let mut capture_spec_map = HashMap::new();
+ for x in capture_specs.into_iter() {
+ capture_spec_map.insert(x.variable, (x.pre, x.post));
+ }
+
+ // assemble the pre types
+ for (capture, ty) in meta.captures.iter().zip(meta.capture_tys.iter()) {
+ if !capture.place.projections.is_empty() {
+ info!("processing capture {:?}", capture);
+ warn!("ignoring place projection in translation of capture: {:?}", capture);
+ // TODO: could handle this by parsing capture strings in specs
+ //unimplemented!("only support specifying closure captures without projections");
+ }
+ let base = capture.var_ident.name.as_str();
+ if let Some((_, (pre, post))) = capture_spec_map.remove_entry(base) {
+ // we kinda want to specify the thing independently of how it is captured
+ match capture.info.capture_kind {
+ ty::UpvarCapture::ByValue => {
+ // full ownership
+ let (processed_ty, _) = self.make_type_with_ref(&pre, ty);
+ pre_types.push(processed_ty);
+
+ if let Some(post) = post {
+ // this should not contain any post
+ return Err(format!(
+ "Did not expect postcondition {:?} for by-value capture",
+ post
+ ));
+ //let (processed_post, _) = self.make_type_with_ref(&post, ty);
+ //post_patterns.push(processed_post.1);
+ }
+ },
+ ty::UpvarCapture::ByRef(ty::BorrowKind::ImmBorrow) => {
+ // shared borrow
+ // if there's a manually specified type, we need to wrap it in the reference
+ if let specs::Type::ShrRef(box auto_type, lft) = ty {
+ let (processed_ty, _) = self.make_type_with_ref(&pre, auto_type);
+ // now wrap it in a shared reference again
+ let altered_ty = specs::Type::ShrRef(Box::new(processed_ty.0), lft.clone());
+ let altered_rfn = format!("#({})", processed_ty.1);
+ pre_types.push(specs::TypeWithRef::new(altered_ty, altered_rfn.clone()));
+
+ // push the same pattern for the post, no ghost variable
+ post_patterns.push(CapturePostRfn::ImmutOrConsume(altered_rfn));
+ }
+ },
+ ty::UpvarCapture::ByRef(_) => {
+ // mutable borrow
+ // we handle ty::BorrowKind::MutBorrow and ty::BorrowKind::UniqImmBorrow
+ // the same way, as they are not really different for RefinedRust's type
+ // system
+ if let specs::Type::MutRef(box auto_type, lft) = ty {
+ let (processed_ty, _) = self.make_type_with_ref(&pre, auto_type);
+ // now wrap it in a mutable reference again
+ // we create a ghost variable
+ let ghost_var = format!("_γ{base}");
+ new_ghost_vars.push(ghost_var.clone());
+ let altered_ty = specs::Type::MutRef(Box::new(processed_ty.0), lft.clone());
+ let altered_rfn = format!("(#({}), {ghost_var})", processed_ty.1);
+ pre_types.push(specs::TypeWithRef::new(altered_ty, altered_rfn));
+
+ if let Some(post) = post {
+ post_patterns.push(CapturePostRfn::Mut(post.rfn.to_string(), ghost_var));
+ } else {
+ // push the same pattern for the post
+ post_patterns.push(CapturePostRfn::Mut(processed_ty.1, ghost_var));
+ }
+ }
+ },
+ }
+ } else {
+ return Err(format!("ambiguous specification of capture {:?}", capture));
+ }
+ }
+
+ // push everything to the builder
+ for x in new_ghost_vars.into_iter() {
+ builder.spec.add_param(radium::CoqName::Named(x), radium::CoqType::Gname).unwrap();
+ }
+
+ // assemble a string for the closure arg
+ let mut pre_rfn = String::new();
+ let mut pre_tys = Vec::new();
+
+ if pre_types.is_empty() {
+ write!(pre_rfn, "()").unwrap();
+ } else {
+ write!(pre_rfn, "-[").unwrap();
+ let mut needs_sep = false;
+ for x in pre_types.into_iter() {
+ if needs_sep {
+ write!(pre_rfn, "; ").unwrap();
+ }
+ needs_sep = true;
+ write!(pre_rfn, "#({})", x.1).unwrap();
+ pre_tys.push(x.0);
+ }
+ write!(pre_rfn, "]").unwrap();
+ }
+ let tuple = make_tuple(pre_tys);
+
+ match meta.kind {
+ ty::ClosureKind::FnOnce => {
+ builder.spec.add_arg(specs::TypeWithRef::new(tuple, pre_rfn))?;
+
+ // generate observations on all the mut-ref captures
+ for p in post_patterns.into_iter() {
+ match p {
+ CapturePostRfn::ImmutOrConsume(_) => {
+ // nothing mutated
+ },
+ CapturePostRfn::Mut(pat, gvar) => {
+ // add an observation on `gvar`
+ builder.spec.add_postcondition(MetaIProp::Observe(gvar, pat).into())?;
+ },
+ }
+ }
+ },
+ ty::ClosureKind::Fn => {
+ // wrap the argument in a shared reference
+ // all the captures are by shared ref
+
+ let lft = meta.closure_lifetime.unwrap();
+ let ref_ty = specs::Type::ShrRef(Box::new(tuple), lft);
+ let ref_rfn = format!("#{}", pre_rfn);
+
+ builder.spec.add_arg(specs::TypeWithRef::new(ref_ty, ref_rfn))?;
+ },
+ ty::ClosureKind::FnMut => {
+ // wrap the argument in a mutable reference
+ let post_name = "__γclos";
+ builder
+ .spec
+ .add_param(radium::CoqName::Named(post_name.to_string()), radium::CoqType::Gname)
+ .unwrap();
+
+ let lft = meta.closure_lifetime.unwrap();
+ let ref_ty = specs::Type::MutRef(Box::new(tuple), lft);
+ let ref_rfn = format!("(#({}), {})", pre_rfn, post_name);
+
+ builder.spec.add_arg(specs::TypeWithRef::new(ref_ty, ref_rfn))?;
+
+ // assemble a postcondition on the closure
+ // we observe on the outer mutable reference for the capture, not on the individual
+ // references
+ let mut post_term = String::new();
+
+ write!(post_term, "-[").unwrap();
+ let mut needs_sep = false;
+ for p in post_patterns.into_iter() {
+ if needs_sep {
+ write!(post_term, "; ").unwrap();
+ }
+ needs_sep = true;
+ match p {
+ CapturePostRfn::ImmutOrConsume(pat) => write!(post_term, "#({pat})").unwrap(),
+ CapturePostRfn::Mut(pat, gvar) => {
+ write!(post_term, "#(#({pat}), {gvar})").unwrap();
+ },
+ }
+ }
+ write!(post_term, "]").unwrap();
+
+ builder
+ .spec
+ .add_postcondition(MetaIProp::Observe(post_name.to_string(), post_term).into())?;
+ },
+ }
+ Ok(())
+ }
+}
+
impl<'a, 'def, F> FunctionSpecParser<'def> for VerboseFunctionSpecParser<'a, 'def, F>
where
F: Fn(specs::LiteralType) -> specs::LiteralTypeRef<'def>,
{
+ fn parse_closure_spec<'tcx, 'b, 'c, H>(
+ &'b mut self,
+ attrs: &'b [&'b AttrItem],
+ spec: &'b mut radium::FunctionBuilder<'def>,
+ closure_meta: ClosureMetaInfo<'c, 'tcx, 'def>,
+ make_tuple: H,
+ ) -> Result<(), String>
+ where
+ H: Fn(Vec<specs::Type<'def>>) -> specs::Type<'def>,
+ {
+ if attrs.len() > 0 {
+ spec.spec.have_spec();
+ }
+
+ // clone to be able to mutably borrow later
+ let builder = spec;
+ let meta: &[specs::LiteralTyParam] = builder.get_ty_params();
+ let lfts: Vec<(Option<String>, specs::Lft)> = builder.get_lfts();
+ let meta: ParseMeta = (&meta, &lfts);
+ info!("ty params: {:?}", meta);
+
+ // TODO: handle args in the common function differently
+ let mut capture_specs = Vec::new();
+
+ // parse captures -- we need to handle it before the other annotations because we will have
+ // to add the first arg for the capture
+ for &it in attrs.iter() {
+ let ref path_segs = it.path.segments;
+ let ref args = it.args;
+
+ let meta: &[specs::LiteralTyParam] = builder.get_ty_params();
+ let meta: ParseMeta = (&meta, &lfts);
+
+ if let Some(seg) = path_segs.get(1) {
+ let buffer = parse::ParseBuffer::new(&args.inner_tokens());
+ let name = &*seg.ident.name.as_str();
+ match name {
+ "capture" => {
+ let spec: ClosureCaptureSpec = buffer.parse(&meta).map_err(str_err)?;
+ capture_specs.push(spec);
+ },
+ _ => {},
+ }
+ }
+ }
+
+ self.merge_capture_information(capture_specs, closure_meta, make_tuple, &mut *builder)?;
+
+ for &it in attrs.iter() {
+ let ref path_segs = it.path.segments;
+ let ref args = it.args;
+
+ if let Some(seg) = path_segs.get(1) {
+ let buffer = parse::ParseBuffer::new(&it.args.inner_tokens());
+ let name = &*seg.ident.name.as_str();
+
+ match self.handle_common_attributes(name, &buffer, builder, &lfts) {
+ Ok(b) => {
+ if !b {
+ if name != "capture" {
+ info!("ignoring function attribute: {:?}", args);
+ }
+ }
+ },
+ Err(e) => {
+ return Err(e);
+ },
+ }
+ }
+ }
+
+ Ok(())
+ }
+
fn parse_function_spec(
&mut self,
attrs: &[&AttrItem],
@@ -226,96 +679,24 @@ where
let ref path_segs = it.path.segments;
let ref args = it.args;
- let meta: &[specs::LiteralTyParam] = builder.get_ty_params();
- let meta: ParseMeta = (&meta, &lfts);
-
if let Some(seg) = path_segs.get(1) {
let buffer = parse::ParseBuffer::new(&it.args.inner_tokens());
- match &*seg.ident.name.as_str() {
- "params" => {
- let params = RRParams::parse(&buffer, &meta).map_err(str_err)?;
- for p in params.params {
- builder.spec.add_param(p.name, p.ty)?;
- }
- },
- "param" => {
- let param = RRParam::parse(&buffer, &meta).map_err(str_err)?;
- builder.spec.add_param(param.name, param.ty)?;
- },
- "args" => {
- let args = RRArgs::parse(&buffer, &meta).map_err(str_err)?;
- if self.arg_types.len() != args.args.len() {
- return Err("wrong number of function arguments given".to_string());
- }
- for (arg, ty) in args.args.into_iter().zip(self.arg_types) {
- let (ty, hint) = self.make_type_with_ref(&arg, ty);
- builder.spec.add_arg(ty)?;
- if let Some(cty) = hint {
- // potentially add a typing hint to the refinement
- if let IdentOrTerm::Ident(ref i) = arg.rfn {
- info!("Trying to add a typing hint for {}", i);
- builder
- .spec
- .add_param_type_annot(&specs::CoqName::Named(i.clone()), cty)?;
- }
+
+ match self.handle_common_attributes(&*seg.ident.name.as_str(), &buffer, builder, &lfts) {
+ Ok(b) => {
+ if !b {
+ let meta: &[specs::LiteralTyParam] = builder.get_ty_params();
+ let meta: ParseMeta = (&meta, &lfts);
+
+ match &*seg.ident.name.as_str() {
+ _ => {
+ info!("ignoring function attribute: {:?}", args);
+ },
}
}
},
- "requires" => {
- let iprop = MetaIProp::parse(&buffer, &meta).map_err(str_err)?;
- builder.spec.add_precondition(iprop.into())?;
- },
- "ensures" => {
- let iprop = MetaIProp::parse(&buffer, &meta).map_err(str_err)?;
- builder.spec.add_postcondition(iprop.into())?;
- },
- "observe" => {
- let m = || {
- let gname: parse::LitStr = buffer.parse(&meta)?;
- buffer.parse::<_, parse::MToken![:]>(&meta)?;
-
- let term: parse::LitStr = buffer.parse(&meta)?;
- let (term, _) = process_coq_literal(&term.value(), meta);
- Ok(MetaIProp::Observe(gname.value().to_string(), term))
- };
- let m = m().map_err(str_err)?;
- builder.spec.add_postcondition(m.into())?;
- },
- "returns" => {
- let tr = LiteralTypeWithRef::parse(&buffer, &meta).map_err(str_err)?;
- // convert to type
- let (ty, _) = self.make_type_with_ref(&tr, self.ret_type);
- builder.spec.set_ret_type(ty)?;
- },
- "exists" => {
- let params = RRParams::parse(&buffer, &meta).map_err(str_err)?;
- for param in params.params.into_iter() {
- builder.spec.add_existential(param.name, param.ty)?;
- }
- },
- "tactics" => {
- let tacs = parse::LitStr::parse(&buffer, &meta).map_err(str_err)?;
- let tacs = tacs.value();
- builder.add_manual_tactic(&tacs);
- },
- "context" => {
- let context_item = RRCoqContextItem::parse(&buffer, &meta).map_err(str_err)?;
- if context_item.at_end {
- builder.spec.add_late_coq_param(
- specs::CoqName::Unnamed,
- specs::CoqType::Literal(context_item.item),
- true,
- )?;
- } else {
- builder.spec.add_coq_param(
- specs::CoqName::Unnamed,
- specs::CoqType::Literal(context_item.item),
- true,
- )?;
- }
- },
- _ => {
- info!("ignoring function attribute: {:?}", args);
+ Err(e) => {
+ return Err(e);
},
}
}
diff --git a/rr_frontend/translation/src/traits.rs b/rr_frontend/translation/src/traits.rs
new file mode 100644
index 0000000000000000000000000000000000000000..6d87263c0ac2b1fbdf86eedadc6b6254506ec8c0
--- /dev/null
+++ b/rr_frontend/translation/src/traits.rs
@@ -0,0 +1,171 @@
+/// Inspired by (in terms of rustc APIs used) by
+/// https://github.com/xldenis/creusot/blob/9d8b1822cd0c43154a6d5d4d05460be56710399c/creusot/src/translation/traits.rs
+use log::info;
+use rustc_hir::def_id::DefId;
+use rustc_infer::infer::TyCtxtInferExt;
+use rustc_middle::ty::{
+ AssocItem, AssocItemContainer, GenericArgsRef, ParamEnv, TraitRef, TyCtxt, TypeVisitableExt,
+};
+use rustc_trait_selection::traits::ImplSource;
+
+pub(crate) fn associated_items(tcx: TyCtxt, def_id: DefId) -> impl Iterator<Item = &AssocItem> {
+ tcx.associated_items(def_id).in_definition_order()
+}
+
+/// Resolve an implementation of a trait using codegen candidate selection.
+/// `did` can be the id of a trait, or the id of an associated item of a trait.
+pub fn resolve_impl_source<'tcx>(
+ tcx: TyCtxt<'tcx>,
+ param_env: ParamEnv<'tcx>,
+ did: DefId,
+ substs: GenericArgsRef<'tcx>,
+) -> Option<&'tcx ImplSource<'tcx, ()>> {
+ let substs = tcx.normalize_erasing_regions(param_env, substs);
+
+ // Check if the `did` is an associated item
+ let trait_ref;
+ if let Some(item) = tcx.opt_associated_item(did) {
+ match item.container {
+ AssocItemContainer::TraitContainer =>
+ // this is part of a trait declaration
+ {
+ trait_ref = TraitRef::new(tcx, item.container_id(tcx), substs)
+ },
+ AssocItemContainer::ImplContainer =>
+ // this is part of an implementation of a trait
+ {
+ trait_ref = tcx.impl_trait_ref(item.container_id(tcx))?.instantiate(tcx, substs)
+ },
+ }
+ } else {
+ // Otherwise, check if it's a reference to a trait itself
+ if tcx.is_trait(did) {
+ trait_ref = TraitRef::new(tcx, did, substs)
+ } else {
+ return None;
+ }
+ };
+
+ let source = tcx.codegen_select_candidate((param_env, trait_ref));
+ source.map_or_else(|_| None, |x| Some(x))
+}
+
+pub fn resolve_trait_or_item<'tcx>(
+ tcx: TyCtxt<'tcx>,
+ param_env: ParamEnv<'tcx>,
+ def_id: DefId,
+ substs: GenericArgsRef<'tcx>,
+) -> Option<(DefId, GenericArgsRef<'tcx>, TraitResolutionKind)> {
+ if tcx.is_trait(def_id) {
+ resolve_trait(tcx, param_env, def_id, substs)
+ } else {
+ resolve_assoc_item(tcx, param_env, def_id, substs)
+ }
+}
+
+/// Resolve a reference to a trait using codegen trait selection.
+/// `did` should be the id of a trait.
+pub fn resolve_trait<'tcx>(
+ tcx: TyCtxt<'tcx>,
+ param_env: ParamEnv<'tcx>,
+ did: DefId,
+ substs: GenericArgsRef<'tcx>,
+) -> Option<(DefId, GenericArgsRef<'tcx>, TraitResolutionKind)> {
+ if tcx.is_trait(did) {
+ let impl_source = resolve_impl_source(tcx, param_env, did, substs);
+ info!("trait impl_source for {:?}: {:?}", did, impl_source);
+ match impl_source? {
+ ImplSource::UserDefined(impl_data) => {
+ Some((impl_data.impl_def_id, impl_data.args, TraitResolutionKind::UserDefined))
+ },
+ ImplSource::Param(_) => Some((did, substs, TraitResolutionKind::Param)),
+ ImplSource::Builtin(_, _) => None,
+ }
+ } else {
+ None
+ }
+}
+
+#[derive(Debug, Copy, Clone, PartialEq)]
+pub enum TraitResolutionKind {
+ Param,
+ UserDefined,
+ Closure,
+}
+
+/// Resolve a reference to a trait item using codegen trait selection.
+/// `did` should be the id of a trait item.
+pub fn resolve_assoc_item<'tcx>(
+ tcx: TyCtxt<'tcx>,
+ param_env: ParamEnv<'tcx>,
+ did: DefId,
+ substs: GenericArgsRef<'tcx>,
+) -> Option<(DefId, GenericArgsRef<'tcx>, TraitResolutionKind)> {
+ let assoc = tcx.opt_associated_item(did)?;
+
+ /*
+ // If we're given an associated item that is already on an instance,
+ // we don't need to resolve at all!
+ //
+ // FIXME: not true given specialization!
+ if let AssocItemContainer::ImplContainer = assoc.container {
+ return None;
+ }
+ */
+
+ let trait_ref = TraitRef::from_method(tcx, tcx.trait_of_item(did).unwrap(), substs);
+
+ let impl_source = resolve_impl_source(tcx, param_env, did, substs)?;
+ info!("trait impl_source for {:?}: {:?}", did, impl_source);
+
+ match impl_source {
+ ImplSource::UserDefined(impl_data) => {
+ // this is a user-defined trait, and we found the right impl
+ // now map back to the item we were looking for
+ let trait_did = tcx.trait_id_of_impl(impl_data.impl_def_id).unwrap();
+ let trait_def: &'tcx rustc_middle::ty::TraitDef = tcx.trait_def(trait_did);
+
+ // Find the id of the actual associated method we will be running
+ let ancestors = trait_def.ancestors(tcx, impl_data.impl_def_id).unwrap();
+ // find the item we were looking for
+ let leaf_def = ancestors.leaf_def(tcx, assoc.def_id).unwrap_or_else(|| {
+ panic!("{:?} not found in {:?}", assoc, impl_data.impl_def_id);
+ });
+
+ if !leaf_def.is_final() && trait_ref.still_further_specializable() {
+ // return the original id to call
+ return Some((did, substs, TraitResolutionKind::UserDefined));
+ }
+
+ // Translate the original substitution into one on the selected impl method
+ let infcx = tcx.infer_ctxt().build();
+
+ let param_env = param_env.with_reveal_all_normalized(tcx);
+ let substs = substs.rebase_onto(tcx, trait_did, impl_data.args);
+ let substs = rustc_trait_selection::traits::translate_args(
+ &infcx,
+ param_env,
+ impl_data.impl_def_id,
+ substs,
+ leaf_def.defining_node,
+ );
+ let leaf_substs = substs;
+ //let leaf_substs = infcx.tcx.erase_regions(substs);
+
+ Some((leaf_def.item.def_id, leaf_substs, TraitResolutionKind::UserDefined))
+ },
+ ImplSource::Param(_) => Some((did, substs, TraitResolutionKind::Param)),
+ ImplSource::Builtin(_, _) =>
+ // the 0-th parameter should be self
+ // if this is a closure, we want to call that closure
+ {
+ match *substs[0].as_type().unwrap().kind() {
+ // try to get the body
+ rustc_middle::ty::Closure(closure_def_id, closure_substs) => {
+ Some((closure_def_id, closure_substs, TraitResolutionKind::Closure))
+ },
+ _ => unimplemented!(),
+ }
+ },
+ }
+}
diff --git a/rr_frontend/translation/src/type_translator.rs b/rr_frontend/translation/src/type_translator.rs
index e5b5c90f268547d46275273118f1f001e50bb685..b1b8ef352ff37ddfdc611e3ea8a30e781215cbaf 100644
--- a/rr_frontend/translation/src/type_translator.rs
+++ b/rr_frontend/translation/src/type_translator.rs
@@ -9,7 +9,7 @@ use std::collections::{HashMap, HashSet};
use std::fmt::Write;
use std::ops::DerefMut;
-use log::{info, trace};
+use log::{info, trace, warn};
use radium;
use rustc_hir::def_id::DefId;
use rustc_middle::ty;
@@ -62,7 +62,7 @@ pub struct TypeTranslator<'def, 'tcx> {
env: &'def Environment<'tcx>,
/// maps universal lifetime indices (Polonius) to their names. offset by 1 because 0 = static.
- universal_lifetimes: RefCell<Vec<String>>,
+ universal_lifetimes: RefCell<HashMap<ty::RegionVid, String>>,
/// arena for keeping ownership of structs
/// during building, it will be None, afterwards it will always be Some
@@ -134,7 +134,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
TypeTranslator {
env,
generic_scope: RefCell::new(Vec::new()),
- universal_lifetimes: RefCell::new(Vec::new()),
+ universal_lifetimes: RefCell::new(HashMap::new()),
adt_deps: RefCell::new(HashMap::new()),
adt_shims: RefCell::new(HashMap::new()),
struct_arena,
@@ -210,12 +210,13 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
/// lifetimes with given names.
pub fn enter_procedure(
&self,
- ty_params: &ty::GenericArgsRef<'tcx>,
- univ_lfts: Vec<String>,
+ ty_params: ty::GenericArgsRef<'tcx>,
+ univ_lfts: HashMap<ty::RegionVid, String>,
) -> Result<(), TranslationError> {
info!("Entering procedure with ty_params {:?} and univ_lfts {:?}", ty_params, univ_lfts);
- let mut v = Vec::new();
+ let mut v: Vec<Option<radium::LiteralTyParam>> = Vec::new();
+ let mut num_lifetimes = 0;
for gen_arg in ty_params.iter() {
match gen_arg.unpack() {
ty::GenericArgKind::Type(ty) => match ty.kind() {
@@ -242,6 +243,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
},
},
ty::GenericArgKind::Lifetime(r) => {
+ num_lifetimes += 1;
match *r {
ty::RegionKind::ReLateBound(..) | ty::RegionKind::ReEarlyBound(..) => {
// ignore
@@ -262,6 +264,12 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
}
}
+ // for closures, not all lifetime parameters materialize in `ty_params`, so we fill them up
+ // afterwards
+ for _ in 0..(univ_lfts.len() - num_lifetimes) {
+ v.push(None);
+ }
+
self.universal_lifetimes.replace(univ_lfts);
self.generic_scope.replace(v);
Ok(())
@@ -270,15 +278,15 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
/// Leave a procedure and remove the corresponding type parameters from the scope.
pub fn leave_procedure(&self) {
self.generic_scope.replace(Vec::new());
- self.universal_lifetimes.replace(Vec::new());
+ self.universal_lifetimes.replace(HashMap::new());
self.tuple_uses.replace(Vec::new());
self.shim_uses.replace(HashMap::new());
}
- /// Lookup a universal lifetime.
- pub fn lookup_universal_lifetime(&self, lft: ty::RegionVid) -> Option<radium::Lft> {
- // offset by 1 due to static which is at zero
- self.universal_lifetimes.borrow().get(lft.as_usize() - 1).map(|s| s.to_string())
+ /// Lookup a universal region.
+ pub fn lookup_universal_region(&self, lft: ty::RegionVid) -> Option<radium::Lft> {
+ info!("Looking up universal lifetime {:?}", lft);
+ self.universal_lifetimes.borrow().get(&lft).map(|s| s.to_string())
}
/// Try to translate a region to a Caesium lifetime.
@@ -289,8 +297,10 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
match **region {
ty::RegionKind::ReEarlyBound(early) => {
info!("Translating region: EarlyBound {:?}", early);
- // TODO is the index here really the right one?
- //self.lookup_universal_lifetime(early.index)
+ None
+ },
+ ty::RegionKind::ReLateBound(idx, r) => {
+ info!("Translating region: LateBound {:?} {:?}", idx, r);
None
},
ty::RegionKind::RePlaceholder(placeholder) => {
@@ -300,7 +310,12 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
},
ty::RegionKind::ReStatic => Some("static".to_string()),
ty::RegionKind::ReErased => Some("erased".to_string()),
- ty::RegionKind::ReVar(v) => self.lookup_universal_lifetime(v),
+ ty::RegionKind::ReVar(v) => {
+ //self.env.info.mk
+ let r = self.lookup_universal_region(v);
+ info!("Translating region: ReVar {:?} as {:?}", v, r);
+ r
+ },
_ => {
info!("Translating region: {:?}", region);
None
@@ -439,6 +454,12 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
TyKind::Tuple(args) => {
self.generate_tuple_use(args.into_iter(), TranslationState::InFunction).map(|x| Some(x))
},
+ TyKind::Closure(_, args) => {
+ // use the upvar tuple
+ let closure_args = args.as_closure();
+ let upvars = closure_args.upvar_tys();
+ self.generate_tuple_use(upvars.into_iter(), TranslationState::InFunction).map(|x| Some(x))
+ },
_ => Err(TranslationError::UnknownError("not a structlike".to_string())),
}
}
@@ -709,6 +730,22 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
Ok(struct_use)
}
+ pub fn make_tuple_use(&self, translated_tys: Vec<radium::Type<'def>>) -> radium::Type<'def> {
+ let num_components = translated_tys.len();
+ if num_components == 0 {
+ return radium::Type::Unit;
+ }
+
+ let (_, lit) = self.get_tuple_struct_ref(num_components);
+ // TODO: don't generate duplicates
+ //let struct_use = radium::AbstractStructUse::new(struct_ref, translated_tys,
+ // radium::TypeIsRaw::Yes);
+ let struct_use = radium::LiteralTypeUse::new(lit, translated_tys);
+ self.tuple_uses.borrow_mut().push(struct_use.clone());
+
+ radium::Type::Literal(struct_use)
+ }
+
/// Get the struct ref for a tuple with [num_components] components.
fn get_tuple_struct_ref(
&self,
@@ -1389,7 +1426,12 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
TyKind::Ref(region, ty, mutability) => {
let translated_ty = self.translate_type_with_deps(ty, adt_deps)?;
// in case this isn't a universal region, we usually won't care about it.
- let lft = self.translate_region(region).unwrap_or("placeholder_lft".to_string());
+ let lft = if let Some(lft) = self.translate_region(region) {
+ lft
+ } else {
+ warn!("Failed to translate region {:?}", region);
+ format!("placeholder_lft")
+ };
match mutability {
rustc_ast::ast::Mutability::Mut => Ok(radium::Type::MutRef(Box::new(translated_ty), lft)),
@@ -1448,17 +1490,21 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
description: "RefinedRust does currently not support str".to_string(),
}),
TyKind::FnDef(_, _) => Err(TranslationError::Unimplemented {
- description: "translate_type_to_layout: implement FnDef".to_string(),
+ description: "translate_type_with_deps: implement FnDef".to_string(),
}),
TyKind::FnPtr(_) => Err(TranslationError::Unimplemented {
- description: "translate_type_to_layout: implement FnPtr".to_string(),
+ description: format!("translate_type_with_deps: implement FnPtr ({:?})", ty),
}),
TyKind::Dynamic(..) => Err(TranslationError::UnsupportedType {
description: "RefinedRust does currently not trait objects".to_string(),
}),
- TyKind::Closure(..) => Err(TranslationError::UnsupportedType {
- description: "RefinedRust does currently not support closures".to_string(),
- }),
+ TyKind::Closure(_def, closure_args) => {
+ // We replace this with the tuple of the closure's state
+ let clos = closure_args.as_closure();
+
+ let upvar_tys = clos.tupled_upvars_ty();
+ self.translate_type_with_deps(&upvar_tys, adt_deps)
+ },
TyKind::Generator(..) => Err(TranslationError::UnsupportedType {
description: "RefinedRust does currently not support generators".to_string(),
}),
@@ -1582,6 +1628,10 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
}
},
TyKind::Tuple(_) => Ok(f.index().to_string()),
+ TyKind::Closure(_, _) => {
+ // treat as tuple of upvars
+ Ok(f.index().to_string())
+ },
_ => Err(TranslationError::InvalidLayout),
}
}
diff --git a/theories/lithium/syntax.v b/theories/lithium/syntax.v
index 50d29df724d1cae937dc641df54f13354d4456ca..4cc5f7b86498346b44b9ee94bd9e80d75919c79b 100644
--- a/theories/lithium/syntax.v
+++ b/theories/lithium/syntax.v
@@ -303,6 +303,63 @@ Ltac goal_to_li :=
end.
*)
+(** * Lemmas for working with [li.iterate] *)
+Lemma iterate_elim0 {Σ A} INV (l : list A) F G:
+ ⊢@{iProp Σ} [{ iterate: l {{ x T, return F x T }}; return G }] -∗
+ INV 0%nat -∗
+ □ (∀ i x T, ⌜l !! i = Some x⌠-∗ INV i -∗ F x T -∗ INV (S i) ∗ T) -∗
+ INV (length l) ∗ G.
+Proof.
+ liFromSyntax.
+ iIntros "Hiter Hinv #HF".
+ iInduction l as [|? l] "IH" forall (INV) => /=. { iFrame. }
+ iDestruct ("HF" $! 0%nat with "[//] Hinv Hiter") as "[??]".
+ iDestruct ("IH" $! (λ i, INV (S i)) with "[] [$] [$]") as "$".
+ iIntros "!>" (????) "??". iApply ("HF" $! (S _) with "[//] [$] [$]").
+Qed.
+
+Lemma iterate_elim1 {Σ A B} INV (l : list A) F G (a : B) :
+ ⊢@{iProp Σ} [{ x ↠iterate: l with a {{ x T a, return F x T a }}; return G x }] -∗
+ INV 0%nat a -∗
+ □ (∀ i x T a, ⌜l !! i = Some x⌠-∗ INV i a -∗ F x T a -∗ ∃ a', INV (S i) a' ∗ T a') -∗
+ ∃ a', INV (length l) a' ∗ G a'.
+Proof.
+ liFromSyntax.
+ iIntros "Hiter Hinv #HF".
+ iInduction l as [|x l] "IH" forall (INV a) => /=. { iExists _. iFrame. }
+ iDestruct ("HF" $! 0%nat with "[//] Hinv Hiter") as (?) "[??]".
+ iDestruct ("IH" $! (λ i, INV (S i)) with "[] [$] [$]") as "$".
+ iIntros "!>" (?????) "??". iApply ("HF" $! (S _) with "[//] [$] [$]").
+Qed.
+
+Lemma iterate_elim2 {Σ A B C} INV (l : list A) F G (a : B) (b : C) :
+ ⊢@{iProp Σ} [{ x, y ↠iterate: l with a, b {{ x T a b, return F x T a b }}; return G x y }] -∗
+ INV 0%nat a b -∗
+ □ (∀ i x T a b, ⌜l !! i = Some x⌠-∗ INV i a b -∗ F x T a b -∗ ∃ a' b', INV (S i) a' b' ∗ T a' b') -∗
+ ∃ a' b', INV (length l) a' b' ∗ G a' b'.
+Proof.
+ liFromSyntax.
+ iIntros "Hiter Hinv #HF".
+ iInduction l as [|x l] "IH" forall (INV a b) => /=. { iExists _, _. iFrame. }
+ iDestruct ("HF" $! 0%nat with "[//] Hinv Hiter") as (??) "[??]".
+ iDestruct ("IH" $! (λ i, INV (S i)) with "[] [$] [$]") as "$".
+ iIntros "!>" (??????) "??". iApply ("HF" $! (S _) with "[//] [$] [$]").
+Qed.
+
+Lemma iterate_elim3 {Σ A B C D} INV (l : list A) F G (a : B) (b : C) (c : D) :
+ ⊢@{iProp Σ} [{ x, y, z ↠iterate: l with a, b, c {{ x T a b c, return F x T a b c }}; return G x y z }] -∗
+ INV 0%nat a b c -∗
+ □ (∀ i x T a b c, ⌜l !! i = Some x⌠-∗ INV i a b c -∗ F x T a b c -∗ ∃ a' b' c', INV (S i) a' b' c' ∗ T a' b' c') -∗
+ ∃ a' b' c', INV (length l) a' b' c' ∗ G a' b' c'.
+Proof.
+ liFromSyntax.
+ iIntros "Hiter Hinv #HF".
+ iInduction l as [|x l] "IH" forall (INV a b c) => /=. { iExists _, _, _. iFrame. }
+ iDestruct ("HF" $! 0%nat with "[//] Hinv Hiter") as (???) "[??]".
+ iDestruct ("IH" $! (λ i, INV (S i)) with "[] [$] [$]") as "$".
+ iIntros "!>" (???????) "??". iApply ("HF" $! (S _) with "[//] [$] [$]").
+Qed.
+
Module li_test.
Section test.
diff --git a/theories/rust_typing/automation.v b/theories/rust_typing/automation.v
index e7b29291710958cfeb00659e686a2818559589a7..0636a8b1dd4184dc6100d96733befca8047659b4 100644
--- a/theories/rust_typing/automation.v
+++ b/theories/rust_typing/automation.v
@@ -975,10 +975,24 @@ Ltac solve_goal_normalized_prepare_hook ::=
(** User facing tactic calls *)
-Ltac sidecond_hammer_it :=
+Ltac sidecond_hammer_it :=
prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; try (unfold_common_defs; solve_goal); unsolved_sidecond_hook.
Ltac sidecond_hammer :=
- unshelve sidecond_hammer_it; sidecond_hammer_it
+ (* the first run may spawn further sideconditions *)
+ unshelve sidecond_hammer_it;
+ (* hence run another iteration *)
+ sidecond_hammer_it
+ (* finally, if we still can't solve it, unfold sealed Caesium definitions (like MaxInt).
+ Since this is very expensive, only do this if these definitions are actually involved in the current goal. *)
+ (*first [*)
+ (*match goal with*)
+ (*| |- (MinInt _ ≤ _)%Z => idtac*)
+ (*| |- (_ ≤ MaxInt _)%Z => idtac*)
+ (*| |- (MinInt _ < _)%Z => idtac*)
+ (*| |- (_ < MaxInt _)%Z => idtac*)
+ (*end; *)
+ (*unsafe_unfold_common_caesium_defs; sidecond_hammer_it*)
+ (*| idtac ]*)
.
Ltac sidecond_solver :=
unshelve_sidecond; sidecond_hook.
diff --git a/theories/rust_typing/closures.v b/theories/rust_typing/closures.v
new file mode 100644
index 0000000000000000000000000000000000000000..f9496fc92c4d1a15977da95553b5bd38ab4bd64c
--- /dev/null
+++ b/theories/rust_typing/closures.v
@@ -0,0 +1,246 @@
+From refinedrust Require Import typing.
+From iris Require Import options.
+
+Section function_subsume.
+ Context `{!typeGS Σ}.
+
+ (* If I have f â— F1, then f â— F2. *)
+ (* I can strengthen the precondition and weaken the postcondition *)
+ (*elctx_sat*)
+ (* TODO: think about how closures capture lifetimes in their environment.
+ lifetimes in the capture shouldn't really show up in their spec at trait-level (a purely safety spec).
+ I guess once I want to know something about the captured values (to reason about their functional correctness), I might need to know about lifetimes. However, even then, they should not pose any constraints -- they should just be satisfied, with us only knowing that they live at least as long as the closure body.
+
+ The point is that I want to say that as long as the closure lifetime is alive, all is fine.
+
+
+ How does the justification that this is fine work?
+ Do I explicitly integrate some existential abstraction?
+ i.e. functions can pose the existence of lifetimes, as long as they are alive under the function lifetime
+
+
+ I don't think I can always just subtype that to use the lifetime of the closure. That would definitely break ghostcell etc. And also not everything might be covariant in the lifetime.
+ *)
+ Lemma subsume_function_ptr π v l1 l2 sts1 sts2 lfts {A B : Type} (F1 : prod_vec lft lfts → A → fn_params) (F2 : prod_vec lft lfts → B → fn_params) T :
+ subsume (v â—áµ¥{Ï€} l1 @ function_ptr sts1 F1) (v â—áµ¥{Ï€} l2 @ function_ptr sts2 F2) T :-
+ and:
+ | drop_spatial;
+ (* TODO could also just require that the layouts are compatible *)
+ exhale ⌜sts1 = sts2âŒ;
+ ∀ (κs : prod_vec lft lfts),
+ (* NOTE: this is more restrictive than necessary *)
+ exhale ⌜∀ a b Ï, (F1 κs a).(fp_elctx) Ï = (F2 κs b).(fp_elctx) ÏâŒ;
+ ∀ (b : B),
+ inhale (fp_Pa (F2 κs b) π);
+ ls ↠iterate: fp_atys (F2 κs b) with [] {{ ty T ls,
+ ∀ l : loc,
+ inhale (l â—â‚—[Ï€, Owned false] #(projT2 ty).2 @ â— (projT2 ty).1); return T (ls ++ [l]) }};
+ ∃ (a : A),
+ exhale ⌜length (fp_atys (F1 κs a)) = length (fp_atys (F2 κs b))âŒ%I;
+ iterate: zip ls (fp_atys (F1 κs a)) {{ e T, exhale (e.1 â—â‚—[Ï€, Owned false] #(projT2 e.2).2 @ â— (projT2 e.2).1); return T }};
+ exhale (fp_Pa (F1 κs a) π);
+ (* show that F1.ret implies F2.ret *)
+ ∀ (vr : val) a2,
+ inhale ((F1 κs a).(fp_fr) a2).(fr_R) π;
+ inhale (vr â—áµ¥{Ï€} ((F1 κs a).(fp_fr) a2).(fr_ref) @ ((F1 κs a).(fp_fr) a2).(fr_ty));
+ ∃ b2,
+ exhale ((F2 κs b).(fp_fr) b2).(fr_R) π;
+ exhale (vr â—áµ¥{Ï€} ((F2 κs b).(fp_fr) b2).(fr_ref) @ ((F2 κs b).(fp_fr) b2).(fr_ty));
+ done
+ | exhale ⌜l1 = l2âŒ; return T.
+ Proof.
+ iIntros "(#Ha & (-> & HT))".
+ iIntros "Hv". iFrame.
+ iDestruct "Ha" as "(-> & Ha)".
+ iEval (rewrite /ty_own_val/=) in "Hv".
+ iDestruct "Hv" as "(%fn & %local_sts & -> & Hen & %Halg1 & %Halg2 & #Htf)".
+ iEval (rewrite /ty_own_val/=).
+ iExists fn, local_sts. iR. iFrame.
+ iSplitR. { done. }
+ iR.
+ iNext.
+
+ rewrite /typed_function.
+ iIntros (κs b Ï) "!>".
+ iIntros (Hargly Hlocally lsa lsv).
+ iIntros "(Hcred & Hargs & Hlocals & Hpre)".
+ iSpecialize ("Ha" $! κs).
+ iDestruct "Ha" as "(%Helctx & Ha)".
+ iSpecialize ("Ha" $! b with "Hpre").
+ (*Locate "|".*)
+ (*
+ Search Z.divide.
+ Search aligned_to
+ is_aligned_to
+ iterate_elim0
+ Locate "iterate:".
+ iDestruct ("Ha" with "[Hargs]") as "(%a & %Hlen & Hargs & Hpre & Ha)".
+ *)
+
+
+ Admitted.
+ Definition subsume_function_ptr_inst := [instance subsume_function_ptr].
+ Global Existing Instance subsume_function_ptr_inst | 10.
+ (* TODO: maybe also make this a subsume_full instance *)
+End function_subsume.
+
+
+(*
+trait MyAdd {
+ type Output;
+
+ #[rr::params("x", "y")]
+ #[rr::args("x", "y")]
+ #[rr::exists("z")]
+ #[rr::returns("z")]
+ fn my_add(x: Self, y: Self) -> Self::Output;
+}
+
+impl MyAdd for usize {
+ type Output = usize;
+
+ #[rr::trust_me]
+ #[rr::params("x", "y")]
+ #[rr::args("x", "y")]
+ #[rr::returns("x + y")]
+ fn my_add(x: usize, y: usize) -> usize {
+ x + y
+ }
+}
+ *)
+
+(* this is what monomorphizations of functions taking a generic of this constraint take *)
+Record MyAdd_phys := {
+ MyAdd_Output_st : syn_type;
+
+ MyAdd_my_add_loc : loc;
+ MyAdd_my_add_arg_sts : list syn_type;
+}.
+
+Section rr.
+Context `{!typeGS Σ}.
+
+Record MyAdd_spec := {
+ MyAdd_Output_ty : sigT (λ rt : Type, type rt);
+ MyAdd_my_add_spec : sigT (λ lfts, sigT (λ A, prod_vec lft lfts → A → fn_params));
+}.
+
+Definition MyAdd_base_spec {Self_rt} (self_ty : type Self_rt) {Output_rt} (Output_ty : type Output_rt) : MyAdd_spec := {|
+ MyAdd_Output_ty := existT _ Output_ty;
+ MyAdd_my_add_spec :=
+ existT _ $ existT _ $ (fn(∀ (()) : 0 | (x, y) : Self_rt * Self_rt, (λ _, []); x @ (self_ty), y @ self_ty ; (λ π, True)) → ∃ z : Output_rt, z @ Output_ty ; (λ π, True))
+|}.
+
+Definition MyAdd_has_spec (π : thread_id) (impl: MyAdd_phys) (spec: MyAdd_spec) : iProp Σ :=
+ ⌜ty_syn_type (projT2 spec.(MyAdd_Output_ty)) = impl.(MyAdd_Output_st)⌠∗
+ impl.(MyAdd_my_add_loc) â—áµ¥{Ï€} impl.(MyAdd_my_add_loc) @ function_ptr impl.(MyAdd_my_add_arg_sts) (projT2 $ projT2 spec.(MyAdd_my_add_spec)) ∗
+ True.
+
+End rr.
+
+
+(* impl for usize *)
+Section rr.
+Context `{!typeGS Σ}.
+
+Definition type_of_usizeastraits_MyAdd_my_add :=
+ fn(∀ (()) : 0 | (x, y) : (_ * _), (λ Ï, []); x @ (int USize), y @ (int USize); (λ Ï€ : thread_id, True))
+ → ∃ _ : unit, x + y @ (int USize); (λ π : thread_id, True).
+
+Definition MyAdd_usize_spec : MyAdd_spec := {|
+ MyAdd_Output_ty := existT _ (int usize_t);
+ MyAdd_my_add_spec := existT _ (existT _ type_of_usizeastraits_MyAdd_my_add);
+|}.
+
+(* Now I need to show: a concrete specification implies the general specification. *)
+Lemma MyAdd_usize_spec_implies_general_spec π impl :
+ MyAdd_has_spec π impl (MyAdd_usize_spec) -∗
+ MyAdd_has_spec π impl (MyAdd_base_spec (int usize_t) (projT2 $ MyAdd_usize_spec.(MyAdd_Output_ty))).
+Proof.
+ iIntros "(%Houtput & Hmyadd & _)".
+ iSplit; first done.
+ iSplitL; last done.
+ simpl.
+ (* TODO use function subtyping *)
+Abort.
+
+End rr.
+
+(** Q: How do we automate this?
+
+ i.e. when we assume a generic thing implementing a trait, we would generally assume that it's implementing the base spec.
+ So we should probably have some lemmas that do a subsumption to the general spec.
+ these should just do subtyping on the function specs.
+
+ Note: In general, we should also have the option for a function to assume a stronger spec, i.e. specify the spec it assumes manually. In particular, this will be quite useful for closures: for functional specs we will want to assume some things about how closures behave.
+*)
+
+
+
+
+(** Closures *)
+Record FnOnce_phys := {
+ FnOnce_Output_st : syn_type;
+ FnOnce_call_once_loc : loc;
+ FnOnce_call_once_arg_sts : list syn_type;
+}.
+Record Fn_phys := {
+ Fn_Output_st : syn_type;
+ Fn_call_loc : loc;
+ Fn_call_arg_sts : list syn_type;
+}.
+Record FnMut_phys := {
+ FnMut_Output_st : syn_type;
+ FnMut_call_mut_loc : loc;
+ FnMut_call_mut_arg_sts : list syn_type;
+}.
+
+Section rr.
+Context `{!typeGS Σ}.
+
+(** FnOnce *)
+Record FnOnce_spec := {
+ FnOnce_Output_ty : sigT (λ rt : Type, type rt);
+ FnOnce_call_once_spec : sigT (λ lfts, sigT (λ A, prod_vec lft lfts → A → fn_params));
+}.
+Definition FnOnce_base_spec {Self_rt} (self_ty : type Self_rt) {Args_rt} (args_ty : type Args_rt) {Output_rt} (Output_ty : type Output_rt) : FnOnce_spec := {|
+ FnOnce_Output_ty := existT _ Output_ty;
+ FnOnce_call_once_spec :=
+ existT _ $ existT _ $ (fn(∀ (()) : 0 | (x, y) : Self_rt * Args_rt, (λ _, []); x @ (self_ty), y @ args_ty ; (λ π, True)) → ∃ z : Output_rt, z @ Output_ty ; (λ π, True));
+|}.
+Definition FnOnce_has_spec (π : thread_id) (impl: FnOnce_phys) (spec: FnOnce_spec) : iProp Σ :=
+ ⌜ty_syn_type (projT2 spec.(FnOnce_Output_ty)) = impl.(FnOnce_Output_st)⌠∗
+ impl.(FnOnce_call_once_loc) â—áµ¥{Ï€} impl.(FnOnce_call_once_loc) @ function_ptr impl.(FnOnce_call_once_arg_sts) (projT2 $ projT2 spec.(FnOnce_call_once_spec)) ∗
+ True.
+
+(** Fn *)
+Record Fn_spec := {
+ Fn_Output_ty : sigT (λ rt : Type, type rt);
+ Fn_call_spec : sigT (λ lfts, sigT (λ A, prod_vec lft lfts → A → fn_params));
+}.
+Definition Fn_base_spec {Self_rt} (self_ty : type Self_rt) {Args_rt} (args_ty : type Args_rt) {Output_rt} (Output_ty : type Output_rt) : Fn_spec := {|
+ Fn_Output_ty := existT _ Output_ty;
+ Fn_call_spec :=
+ existT _ $ existT _ $ (fn(∀ ((), κ) : 1 | (x, y) : Self_rt * Args_rt, (λ _, []); #x @ (shr_ref self_ty κ), y @ args_ty ; (λ π, True)) → ∃ z : Output_rt, z @ Output_ty ; (λ π, True));
+|}.
+Definition Fn_has_spec (π : thread_id) (impl: Fn_phys) (spec: Fn_spec) : iProp Σ :=
+ ⌜ty_syn_type (projT2 spec.(Fn_Output_ty)) = impl.(Fn_Output_st)⌠∗
+ impl.(Fn_call_loc) â—áµ¥{Ï€} impl.(Fn_call_loc) @ function_ptr impl.(Fn_call_arg_sts) (projT2 $ projT2 spec.(Fn_call_spec)) ∗
+ True.
+
+(** FnMut *)
+Record FnMut_spec := {
+ FnMut_Output_ty : sigT (λ rt : Type, type rt);
+ FnMut_call_mut_spec : sigT (λ lfts, sigT (λ A, prod_vec lft lfts → A → fn_params));
+}.
+Definition FnMut_base_spec {Self_rt} (self_ty : type Self_rt) {Args_rt} (args_ty : type Args_rt) {Output_rt} (Output_ty : type Output_rt) : FnMut_spec := {|
+ FnMut_Output_ty := existT _ Output_ty;
+ FnMut_call_mut_spec :=
+ existT _ $ existT _ $ (fn(∀ ((), κ) : 1 | (x, y, γ) : Self_rt * Args_rt * gname, (λ _, []); (#x, γ) @ (mut_ref self_ty κ), y @ args_ty ; (λ π, True)) → ∃ (z, x') : Output_rt * Self_rt, z @ Output_ty ; (λ π, gvar_pobs γ x'));
+|}.
+Definition FnMut_has_spec (π : thread_id) (impl: FnMut_phys) (spec: FnMut_spec) : iProp Σ :=
+ ⌜ty_syn_type (projT2 spec.(FnMut_Output_ty)) = impl.(FnMut_Output_st)⌠∗
+ impl.(FnMut_call_mut_loc) â—áµ¥{Ï€} impl.(FnMut_call_mut_loc) @ function_ptr impl.(FnMut_call_mut_arg_sts) (projT2 $ projT2 spec.(FnMut_call_mut_spec)) ∗
+ True.
+
+End rr.