Support closures (with simple usage of traits)

src/analyze.rs

@@ -340,4 +340,26 @@ impl<'tcx> Analyzer<'tcx> {
             self.tcx.dcx().err(format!("verification error: {:?}", err));
         }
     }
+
+    // replacement of `self.tcx.fn_sig(local_def_id).instantiate_identity().skip_binder()`
+    // to workaround the following error when used with closures:
+    // > to get the signature of a closure, use `args.as_closure().sig()` not `fn_sig()`
+    pub fn local_fn_sig(&self, local_def_id: LocalDefId) -> mir_ty::FnSig<'tcx> {
+        let ty = self.tcx.type_of(local_def_id).instantiate_identity();
+        let sig = if let mir_ty::TyKind::Closure(_, substs) = ty.kind() {
+            substs.as_closure().sig().skip_binder()
+        } else {
+            ty.fn_sig(self.tcx).skip_binder()
+        };
+
+        // take input/output from MIR body to obtain lifted closure function type
+        let body = self.tcx.optimized_mir(local_def_id);
+        self.tcx.mk_fn_sig(
+            body.args_iter().map(|arg| body.local_decls[arg].ty),
+            body.return_ty(),
+            sig.c_variadic,
+            sig.unsafety,
+            sig.abi,
+        )
+    }
 }

src/analyze/basic_block.rs

@@ -84,16 +84,54 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     ) -> Vec<chc::Clause> {
         let mut clauses = Vec::new();
 
-        if expected_args.is_empty() {
-            // elaboration: we need at least one predicate variable in parameter (see mir_function_ty_impl)
-            expected_args.push(rty::RefinedType::unrefined(rty::Type::unit()).vacuous());
-        }
         tracing::debug!(
             got = %got.display(),
             expected = %crate::pretty::FunctionType::new(&expected_args, &expected_ret).display(),
             "fn_sub_type"
         );
 
+        match got.abi {
+            rty::FunctionAbi::Rust => {
+                if expected_args.is_empty() {
+                    // elaboration: we need at least one predicate variable in parameter (see mir_function_ty_impl)
+                    expected_args.push(rty::RefinedType::unrefined(rty::Type::unit()).vacuous());
+                }
+            }
+            rty::FunctionAbi::RustCall => {
+                // &Closure, { v: (own i32, own bool) | v = (<0>, <false>) }
+                // =>
+                // &Closure, { v: i32 | (<v>, _) = (<0>, <false>) }, { v: bool | (_, <v>) = (<0>, <false>) }
+
+                let rty::RefinedType { ty, mut refinement } =
+                    expected_args.pop().expect("rust-call last arg");
+                let ty = ty.into_tuple().expect("rust-call last arg is tuple");
+                let mut replacement_tuple = Vec::new(); // will be (<v>, _) or (_, <v>)
+                for elem in &ty.elems {
+                    let existential = refinement.existentials.push(elem.ty.to_sort());
+                    replacement_tuple.push(chc::Term::var(rty::RefinedTypeVar::Existential(
+                        existential,
+                    )));
+                }
+
+                for (i, elem) in ty.elems.into_iter().enumerate() {
+                    let mut param_ty = elem.deref();
+                    param_ty
+                        .refinement
+                        .push_conj(refinement.clone().subst_value_var(|| {
+                            let mut value_elems = replacement_tuple.clone();
+                            value_elems[i] = chc::Term::var(rty::RefinedTypeVar::Value).boxed();
+                            chc::Term::tuple(value_elems)
+                        }));
+                    expected_args.push(param_ty);
+                }
+
+                tracing::info!(
+                    expected = %crate::pretty::FunctionType::new(&expected_args, &expected_ret).display(),
+                    "rust-call expanded",
+                );
+            }
+        }
+
         // TODO: check sty and length is equal
         let mut builder = self.env.build_clause();
         for (param_idx, param_rty) in got.params.iter_enumerated() {
@@ -125,11 +163,114 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         clauses
     }
 
+    fn const_bytes_ty(
+        &self,
+        ty: mir_ty::Ty<'tcx>,
+        alloc: mir::interpret::ConstAllocation,
+        range: std::ops::Range<usize>,
+    ) -> PlaceType {
+        let alloc = alloc.inner();
+        let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(range);
+        match ty.kind() {
+            mir_ty::TyKind::Str => {
+                let content = std::str::from_utf8(bytes).unwrap();
+                PlaceType::with_ty_and_term(
+                    rty::Type::string(),
+                    chc::Term::string(content.to_owned()),
+                )
+            }
+            mir_ty::TyKind::Bool => {
+                PlaceType::with_ty_and_term(rty::Type::bool(), chc::Term::bool(bytes[0] != 0))
+            }
+            mir_ty::Int(_) => {
+                // TODO: see target endianess
+                let val = match bytes.len() {
+                    1 => i8::from_ne_bytes(bytes.try_into().unwrap()) as i64,
+                    2 => i16::from_ne_bytes(bytes.try_into().unwrap()) as i64,
+                    4 => i32::from_ne_bytes(bytes.try_into().unwrap()) as i64,
+                    8 => i64::from_ne_bytes(bytes.try_into().unwrap()),
+                    _ => unimplemented!("const int bytes len: {}", bytes.len()),
+                };
+                PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(val))
+            }
+            _ => unimplemented!("const bytes ty: {:?}", ty),
+        }
+    }
+
+    fn const_value_ty(&self, val: &mir::ConstValue<'tcx>, ty: &mir_ty::Ty<'tcx>) -> PlaceType {
+        use mir::{interpret::Scalar, ConstValue, Mutability};
+        match (ty.kind(), val) {
+            (mir_ty::TyKind::Int(_), ConstValue::Scalar(Scalar::Int(val))) => {
+                let val = val.try_to_int(val.size()).unwrap();
+                PlaceType::with_ty_and_term(
+                    rty::Type::int(),
+                    chc::Term::int(val.try_into().unwrap()),
+                )
+            }
+            (mir_ty::TyKind::Bool, ConstValue::Scalar(Scalar::Int(val))) => {
+                PlaceType::with_ty_and_term(
+                    rty::Type::bool(),
+                    chc::Term::bool(val.try_to_bool().unwrap()),
+                )
+            }
+            (mir_ty::TyKind::Tuple(tys), _) if tys.is_empty() => {
+                PlaceType::with_ty_and_term(rty::Type::unit(), chc::Term::tuple(vec![]))
+            }
+            (
+                mir_ty::TyKind::Ref(_, elem, Mutability::Not),
+                ConstValue::Scalar(Scalar::Ptr(ptr, _)),
+            ) => {
+                // Pointer::into_parts is OK for CtfeProvenance
+                // in later version of rustc it has prov_and_relative_offset that ensures this
+                let (prov, offset) = ptr.into_parts();
+                let global_alloc = self.tcx.global_alloc(prov.alloc_id());
+                match global_alloc {
+                    mir::interpret::GlobalAlloc::Memory(alloc) => {
+                        let layout = self
+                            .tcx
+                            .layout_of(mir_ty::ParamEnv::reveal_all().and(*elem))
+                            .unwrap();
+                        let size = layout.size;
+                        let range =
+                            offset.bytes() as usize..(offset.bytes() + size.bytes()) as usize;
+                        self.const_bytes_ty(*elem, alloc, range).immut()
+                    }
+                    _ => unimplemented!("const ptr alloc: {:?}", global_alloc),
+                }
+            }
+            (mir_ty::TyKind::Ref(_, elem, Mutability::Not), ConstValue::Slice { data, meta }) => {
+                let end = (*meta).try_into().unwrap();
+                self.const_bytes_ty(*elem, *data, 0..end).immut()
+            }
+            _ => unimplemented!("const: {:?}, ty: {:?}", val, ty),
+        }
+    }
+
+    fn const_ty(&self, const_: &mir::Const<'tcx>) -> PlaceType {
+        match const_ {
+            mir::Const::Val(val, ty) => self.const_value_ty(val, ty),
+            mir::Const::Unevaluated(unevaluated, ty) => {
+                // since all constants are immutable in current setup,
+                // it should be okay to evaluate them here on-the-fly
+                let param_env = self.tcx.param_env(self.local_def_id);
+                let val = self
+                    .tcx
+                    .const_eval_resolve(param_env, *unevaluated, None)
+                    .unwrap();
+                self.const_value_ty(&val, ty)
+            }
+            _ => unimplemented!("const: {:?}", const_),
+        }
+    }
+
     fn operand_type(&self, mut operand: Operand<'tcx>) -> PlaceType {
         if let Operand::Copy(p) | Operand::Move(p) = &mut operand {
             *p = self.elaborate_place(p);
         }
-        let ty = self.env.operand_type(operand.clone());
+        let ty = match &operand {
+            Operand::Copy(place) | Operand::Move(place) => self.env.place_type(*place),
+            Operand::Constant(operand) => self.const_ty(&operand.const_),
+        };
         tracing::debug!(operand = ?operand, ty = %ty.display(), "operand_type");
         ty
     }
@@ -472,9 +613,21 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 rty::FunctionType::new([param1, param2].into_iter().collect(), ret).into()
             }
             Some((def_id, args)) => {
+                let param_env = self.tcx.param_env(self.local_def_id);
+                let instance =
+                    mir_ty::Instance::resolve(self.tcx, param_env, def_id, args).unwrap();
+                let resolved_def_id = if let Some(instance) = instance {
+                    instance.def_id()
+                } else {
+                    def_id
+                };
+                if def_id != resolved_def_id {
+                    tracing::info!(?def_id, ?resolved_def_id, "resolve",);
+                }
+
                 let rty_args = args.types().map(|ty| self.type_builder.build(ty)).collect();
                 self.ctx
-                    .def_ty_with_args(def_id, rty_args)
+                    .def_ty_with_args(resolved_def_id, rty_args)
                     .expect("unknown def")
                     .ty
                     .vacuous()

src/analyze/crate_.rs

@@ -39,18 +39,15 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
 
     #[tracing::instrument(skip(self), fields(def_id = %self.tcx.def_path_str(local_def_id)))]
     fn refine_fn_def(&mut self, local_def_id: LocalDefId) {
+        let sig = self.ctx.local_fn_sig(local_def_id);
+
         let mut analyzer = self.ctx.local_def_analyzer(local_def_id);
 
         if analyzer.is_annotated_as_trusted() {
             assert!(analyzer.is_fully_annotated());
             self.trusted.insert(local_def_id.to_def_id());
         }
 
-        let sig = self
-            .tcx
-            .fn_sig(local_def_id)
-            .instantiate_identity()
-            .skip_binder();
         use mir_ty::TypeVisitableExt as _;
         if sig.has_param() && !analyzer.is_fully_annotated() {
             self.ctx.register_deferred_def(local_def_id.to_def_id());

src/analyze/local_def.rs

@@ -169,8 +169,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     }
 
     pub fn expected_ty(&mut self) -> rty::RefinedType {
-        let sig = self.tcx.fn_sig(self.local_def_id);
-        let sig = sig.instantiate_identity().skip_binder();
+        let sig = self.ctx.local_fn_sig(self.local_def_id);
 
         let mut param_resolver = analyze::annot::ParamResolver::default();
         for (input_ident, input_ty) in self

src/chc.rs

@@ -616,6 +616,10 @@ impl<V> Term<V> {
         Term::Mut(Box::new(t1), Box::new(t2))
     }
 
+    pub fn boxed(self) -> Self {
+        Term::Box(Box::new(self))
+    }
+
     pub fn box_current(self) -> Self {
         Term::BoxCurrent(Box::new(self))
     }

src/refine/env.rs

@@ -2,8 +2,7 @@ use std::collections::{BTreeMap, HashMap};
 
 use pretty::{termcolor, Pretty};
 use rustc_index::IndexVec;
-use rustc_middle::mir::{self, Local, Operand, Place, PlaceElem};
-use rustc_middle::ty as mir_ty;
+use rustc_middle::mir::{Local, Place, PlaceElem};
 use rustc_target::abi::{FieldIdx, VariantIdx};
 
 use crate::chc;
@@ -454,6 +453,14 @@ impl PlaceType {
         builder.build(ty, term)
     }
 
+    pub fn immut(self) -> PlaceType {
+        let mut builder = PlaceTypeBuilder::default();
+        let (inner_ty, inner_term) = builder.subsume(self);
+        let ty = rty::PointerType::immut_to(inner_ty).into();
+        let term = chc::Term::box_(inner_term);
+        builder.build(ty, term)
+    }
+
     pub fn tuple(ptys: Vec<PlaceType>) -> PlaceType {
         let mut builder = PlaceTypeBuilder::default();
         let mut tys = Vec::new();
@@ -951,48 +958,6 @@ impl Env {
         self.var_type(local.into())
     }
 
-    pub fn operand_type(&self, operand: Operand<'_>) -> PlaceType {
-        use mir::{interpret::Scalar, Const, ConstValue, Mutability};
-        match operand {
-            Operand::Copy(place) | Operand::Move(place) => self.place_type(place),
-            Operand::Constant(operand) => {
-                let Const::Val(val, ty) = operand.const_ else {
-                    unimplemented!("const: {:?}", operand.const_);
-                };
-                match (ty.kind(), val) {
-                    (mir_ty::TyKind::Int(_), ConstValue::Scalar(Scalar::Int(val))) => {
-                        let val = val.try_to_int(val.size()).unwrap();
-                        PlaceType::with_ty_and_term(
-                            rty::Type::int(),
-                            chc::Term::int(val.try_into().unwrap()),
-                        )
-                    }
-                    (mir_ty::TyKind::Bool, ConstValue::Scalar(Scalar::Int(val))) => {
-                        PlaceType::with_ty_and_term(
-                            rty::Type::bool(),
-                            chc::Term::bool(val.try_to_bool().unwrap()),
-                        )
-                    }
-                    (
-                        mir_ty::TyKind::Ref(_, elem, Mutability::Not),
-                        ConstValue::Slice { data, meta },
-                    ) if matches!(elem.kind(), mir_ty::TyKind::Str) => {
-                        let end = meta.try_into().unwrap();
-                        let content = data
-                            .inner()
-                            .inspect_with_uninit_and_ptr_outside_interpreter(0..end);
-                        let content = std::str::from_utf8(content).unwrap();
-                        PlaceType::with_ty_and_term(
-                            rty::PointerType::immut_to(rty::Type::string()).into(),
-                            chc::Term::box_(chc::Term::string(content.to_owned())),
-                        )
-                    }
-                    _ => unimplemented!("const: {:?}, ty: {:?}", val, ty),
-                }
-            }
-        }
-    }
-
     fn borrow_var(&mut self, var: Var, prophecy: TempVarIdx) -> PlaceType {
         match *self.flow_binding(var).expect("borrowing unbound var") {
             FlowBinding::Box(x) => {