Support associated consts (e.g. i64::MAX) in annotations

src/analyze.rs

@@ -35,6 +35,25 @@ mod reconstruct_slice_indexing;
 // TODO: organize structure and remove cross dependency between refine
 pub use did_cache::DefIdCache;
 
+fn scalar_const_term<T>(
+    ty: mir_ty::Ty<'_>,
+    val: &mir::ConstValue,
+) -> Option<(rty::Type<T>, chc::Term<T>)> {
+    use mir::interpret::Scalar;
+    match (ty.kind(), val) {
+        (mir_ty::TyKind::Int(_), mir::ConstValue::Scalar(Scalar::Int(v))) => {
+            Some((rty::Type::int(), chc::Term::int(v.to_int(v.size()))))
+        }
+        (mir_ty::TyKind::Uint(_), mir::ConstValue::Scalar(Scalar::Int(v))) => {
+            Some((rty::Type::int(), chc::Term::int(v.to_uint(v.size()))))
+        }
+        (mir_ty::TyKind::Bool, mir::ConstValue::Scalar(Scalar::Int(v))) => {
+            Some((rty::Type::bool(), chc::Term::bool(v.try_to_bool().unwrap())))
+        }
+        _ => None,
+    }
+}
+
 fn fn_operand<'tcx>(
     tcx: TyCtxt<'tcx>,
     def_id: DefId,

src/analyze/annot_fn.rs

@@ -3,6 +3,7 @@ use std::collections::HashMap;
 use pretty::{termcolor, Pretty};
 use rustc_hir::{def_id::LocalDefId, HirId};
 use rustc_index::IndexVec;
+use rustc_middle::mir;
 use rustc_middle::ty::{self as mir_ty, TyCtxt};
 
 use crate::analyze::{self, did_cache::DefIdCache};
@@ -603,6 +604,25 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
         chc::Term::datatype_ctor(d_sym, sort_args, v_sym, field_terms)
     }
 
+    fn const_term(
+        &self,
+        const_did: rustc_span::def_id::DefId,
+        hir: &'tcx rustc_hir::Expr<'tcx>,
+    ) -> chc::Term<rty::FunctionParamIdx> {
+        let ty = self.expr_ty(hir);
+        let generic_args = mir_ty::EarlyBinder::bind(self.typeck.node_args(hir.hir_id))
+            .instantiate(self.tcx, self.generic_args);
+        let typing_env = mir_ty::TypingEnv::fully_monomorphized();
+        let unevaluated = mir::UnevaluatedConst::new(const_did, generic_args);
+        let val = self
+            .tcx
+            .const_eval_resolve(typing_env, unevaluated, hir.span)
+            .unwrap_or_else(|e| panic!("failed to evaluate constant in formula: {:?}", e));
+        let (_, term) = analyze::scalar_const_term(ty, &val)
+            .unwrap_or_else(|| unimplemented!("unsupported constant type in formula: {:?}", ty));
+        term
+    }
+
     fn to_formula_with_quantified_vars(
         &self,
         closure: &rustc_hir::Body<'tcx>,
@@ -743,6 +763,10 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                 ) => {
                     FormulaOrTerm::Term(self.variant_ctor_term(ctor_did, self.expr_ty(hir), vec![]))
                 }
+                rustc_hir::def::Res::Def(
+                    rustc_hir::def::DefKind::Const | rustc_hir::def::DefKind::AssocConst,
+                    const_did,
+                ) => FormulaOrTerm::Term(self.const_term(const_did, hir)),
                 _ => unimplemented!("unsupported path in formula: {:?}", qpath),
             },
             ExprKind::Tup(exprs) => {

src/analyze/basic_block.rs

@@ -435,26 +435,11 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     }
 
     fn const_value_ty(&self, val: &mir::ConstValue, ty: &mir_ty::Ty<'tcx>) -> PlaceType {
+        if let Some((scalar_ty, term)) = analyze::scalar_const_term(*ty, val) {
+            return PlaceType::with_ty_and_term(scalar_ty, term);
+        }
         use mir::{interpret::Scalar, ConstValue, Mutability};
         match (ty.kind(), val) {
-            (mir_ty::TyKind::Int(_), ConstValue::Scalar(Scalar::Int(val))) => {
-                PlaceType::with_ty_and_term(
-                    rty::Type::int(),
-                    chc::Term::int(val.to_int(val.size())),
-                )
-            }
-            (mir_ty::TyKind::Uint(_), ConstValue::Scalar(Scalar::Int(val))) => {
-                PlaceType::with_ty_and_term(
-                    rty::Type::int(),
-                    chc::Term::int(val.to_uint(val.size())),
-                )
-            }
-            (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![]))
             }

tests/ui/fail/assoc_const_annot.rs

@@ -0,0 +1,10 @@
+//@error-in-other-file: Unsat
+
+#[thrust_macros::requires(x == i64::MAX)]
+fn only_max(x: i64) -> i64 {
+    x
+}
+
+fn main() {
+    let _ = only_max(9223372036854775806);
+}

tests/ui/pass/assoc_const_annot.rs

@@ -0,0 +1,10 @@
+//@check-pass
+
+#[thrust_macros::requires(x == i64::MAX)]
+fn only_max(x: i64) -> i64 {
+    x
+}
+
+fn main() {
+    let _ = only_max(9223372036854775807);
+}