tests pass?

flux-rs · Dec 12, 2024 · 180bde5 · 180bde5
1 parent 4c6070e
commit 180bde5
Show file tree

Hide file tree

Showing 13 changed files with 132 additions and 31 deletions.
diff --git a/crates/flux-desugar/src/desugar.rs b/crates/flux-desugar/src/desugar.rs
@@ -480,9 +480,7 @@ impl<'a, 'genv, 'tcx: 'genv> RustItemCtxt<'a, 'genv, 'tcx> {
         let owner_id = self.owner;
         let generics = fhir::Generics::trivial();
         let kind = fhir::ItemKind::Constant(constant_info);
-        let res = Ok(fhir::Item { owner_id, generics, kind });
-        println!("TRACE: desugar_const_info {res:?}");
-        res
+        Ok(fhir::Item { owner_id, generics, kind })
     }
 
     pub(crate) fn desugar_fn_spec(

diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs
@@ -359,6 +359,17 @@ pub(crate) fn conv_invariants(
     cx.conv_invariants(&mut env, invariants)
 }
 
+pub(crate) fn conv_constant(
+    genv: GlobalEnv,
+    constant: &fhir::ConstantInfo,
+    wfckresults: &WfckResults,
+) -> QueryResult<rty::ConstantInfo> {
+    let mut cx = AfterSortck::new(genv, wfckresults).into_conv_ctxt();
+    let mut env = Env::new(&[]);
+    let expr = cx.conv_expr(&mut env, &constant.expr)?;
+    Ok(rty::ConstantInfo { value: Some(expr) })
+}
+
 pub(crate) fn conv_defn(
     genv: GlobalEnv,
     func: &fhir::SpecFunc,
@@ -567,10 +578,11 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
 
     pub(crate) fn conv_constant_info(
         &mut self,
-        def_id: MaybeExternId,
         constant_info: &fhir::ConstantInfo,
     ) -> QueryResult<rty::ConstantInfo> {
-        todo!("CONV constant_info")
+        let mut env = Env::new(&[]);
+        let expr = self.conv_expr(&mut env, &constant_info.expr)?;
+        Ok(rty::ConstantInfo { value: Some(expr) })
     }
 
     pub(crate) fn conv_fn_sig(

diff --git a/crates/flux-fhir-analysis/src/lib.rs b/crates/flux-fhir-analysis/src/lib.rs
@@ -141,7 +141,9 @@ fn adt_def(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<rty::AdtDef> {
 fn constant_info(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<rty::ConstantInfo> {
     let def_id = genv.maybe_extern_id(def_id);
     let item = genv.map().expect_item(def_id.local_id())?;
-    todo!("FOR GODS SAKE {item:?}")
+    let constant = item.expect_constant();
+    let wfckresults = wf::check_constant(genv, item.owner_id, constant)?;
+    conv::conv_constant(genv, constant, &wfckresults)
 }
 
 fn invariants_of(genv: GlobalEnv, item: &fhir::Item) -> QueryResult<Vec<rty::Invariant>> {

diff --git a/crates/flux-fhir-analysis/src/wf/mod.rs b/crates/flux-fhir-analysis/src/wf/mod.rs
@@ -59,6 +59,25 @@ pub(crate) fn check_fn_spec(genv: GlobalEnv, func: &fhir::SpecFunc) -> Result<Wf
     Ok(infcx.into_results())
 }
 
+pub(crate) fn check_constant(
+    genv: GlobalEnv,
+    def_id: MaybeExternId<OwnerId>,
+    constant: &fhir::ConstantInfo,
+) -> Result<WfckResults> {
+    let owner_id = def_id.local_id();
+    let mut infcx = InferCtxt::new(genv, FluxOwnerId::Rust(owner_id));
+    // let mut wf = Wf::new(&mut infcx);
+    let mut err = None;
+    let Ok(Some(sort)) = genv.sort_of_def_id(owner_id.to_def_id()) else {
+        panic!("Unsupported constant {def_id:?}");
+    };
+    infcx
+        .check_expr(&constant.expr, &sort)
+        .collect_err(&mut err);
+    err.into_result()?;
+    Ok(infcx.into_results())
+}
+
 pub(crate) fn check_invariants(
     genv: GlobalEnv,
     adt_def_id: MaybeExternId<OwnerId>,
@@ -225,7 +244,7 @@ impl<'a, 'genv, 'tcx> Wf<'a, 'genv, 'tcx> {
                         cx.conv_generic_predicates(def_id, &item.generics)?;
                     }
                     fhir::ItemKind::Constant(constant_info) => {
-                        cx.conv_constant_info(def_id, constant_info)?;
+                        cx.conv_constant_info(constant_info)?;
                     }
                 }
             }

diff --git a/crates/flux-fhir-analysis/src/wf/sortck.rs b/crates/flux-fhir-analysis/src/wf/sortck.rs
@@ -287,17 +287,10 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> {
         match path.res {
             ExprRes::Param(_, id) => Ok(self.param_sort(id)),
             ExprRes::Const(def_id) => {
-                // TODO(nilehmann) generalize const sorts
-                let ty = self.genv.tcx().type_of(def_id).no_bound_vars().unwrap();
-                if ty.is_integral() {
-                    Ok(rty::Sort::Int)
-                } else if let Some(sort) =
-                    self.genv.sort_of_rust_ty(def_id, ty).unwrap_or_else(|err| {
-                        span_bug!(
-                            path.span,
-                            "unknown sort for `{def_id:?}` of type {ty:?} with {err:?}"
-                        )
-                    })
+                if let Some(sort) = self
+                    .genv
+                    .sort_of_def_id(def_id)
+                    .unwrap_or_else(|_err| span_bug!(path.span, "unknown sort for `{def_id:?}`"))
                 {
                     Ok(sort)
                 } else {

diff --git a/crates/flux-infer/src/fixpoint_encoding.rs b/crates/flux-infer/src/fixpoint_encoding.rs
@@ -1301,10 +1301,11 @@ impl<'genv, 'tcx> ExprEncodingCtxt<'genv, 'tcx> {
                     }
                 } else {
                     let info = self.genv.constant_info(def_id).unwrap();
+                    let sort = self.genv.sort_of_def_id(def_id).unwrap().unwrap();
                     ConstInfo {
                         name: self.global_var_gen.fresh(),
                         comment: format!("rust const: {}", def_id_to_string(def_id)),
-                        sort: scx.sort_to_fixpoint(&info.sort),
+                        sort: scx.sort_to_fixpoint(&sort),
                         val: info.value,
                     }
                 }

diff --git a/crates/flux-middle/src/fhir.rs b/crates/flux-middle/src/fhir.rs
@@ -218,6 +218,14 @@ pub struct Item<'fhir> {
 }
 
 impl<'fhir> Item<'fhir> {
+    pub fn expect_constant(&self) -> &ConstantInfo<'fhir> {
+        if let ItemKind::Constant(constant) = &self.kind {
+            constant
+        } else {
+            bug!("expected constant")
+        }
+    }
+
     pub fn expect_enum(&self) -> &EnumDef<'fhir> {
         if let ItemKind::Enum(enum_def) = &self.kind {
             enum_def

diff --git a/crates/flux-middle/src/queries.rs b/crates/flux-middle/src/queries.rs
@@ -437,11 +437,10 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> {
                 def_id,
                 |def_id| (self.providers.constant_info)(genv, def_id.local_id()),
                 |def_id| genv.cstore().constant_info(def_id),
-                |def_id| {
+                |_def_id| {
                     // todo
-                    let ty = genv.tcx().type_of(def_id).no_bound_vars().unwrap();
-                    let sort = genv.sort_of_rust_ty(def_id, ty)?.unwrap();
-                    Ok(rty::ConstantInfo { def_id, sort, value: None })
+                    // let sort = genv.sort_of_def_id(def_id)?.unwrap();
+                    Ok(rty::ConstantInfo { /* def_id, sort, */ value: None })
                 },
             )
         })

diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs
@@ -968,8 +968,8 @@ pub enum SortArg {
 
 #[derive(Debug, Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable)]
 pub struct ConstantInfo {
-    pub def_id: DefId,
-    pub sort: Sort,
+    // pub def_id: DefId,
+    // pub sort: Sort,
     pub value: Option<Expr>,
 }
 

diff --git a/crates/flux-middle/src/sort_of.rs b/crates/flux-middle/src/sort_of.rs
@@ -28,6 +28,15 @@ impl GlobalEnv<'_, '_> {
         Ok(sort)
     }
 
+    pub fn sort_of_def_id(self, def_id: DefId) -> QueryResult<Option<rty::Sort>> {
+        let ty = self.tcx().type_of(def_id).no_bound_vars().unwrap();
+        if ty.is_integral() {
+            Ok(Some(rty::Sort::Int))
+        } else {
+            self.sort_of_rust_ty(def_id, ty)
+        }
+    }
+
     pub fn sort_of_rust_ty(
         self,
         def_id: DefId,

diff --git a/tests/tests/neg/surface/bitvec_const00.rs b/tests/tests/neg/surface/bitvec_const00.rs
@@ -0,0 +1,33 @@
+#![flux::defs(
+    fn is_start(x:bitvec<32>) -> bool { x == START }
+)]
+
+#[flux::opaque]
+#[flux::refined_by(val: bitvec<32>)]
+pub struct BV32(u32);
+
+impl BV32 {
+    #[flux::trusted]
+    #[flux::sig(fn (x:u32) -> BV32[bv_int_to_bv32(x)])]
+    const fn new(val: u32) -> Self {
+        BV32(val)
+    }
+}
+
+#[flux_rs::constant(bv_int_to_bv32(0x4567))]
+pub const START: BV32 = BV32::new(0x4567);
+
+#[flux_rs::sig(fn () -> BV32[START])]
+pub fn test1() -> BV32 {
+    BV32::new(0x4567)
+}
+
+#[flux_rs::sig(fn () -> BV32{v: is_start(v)})]
+pub fn test2() -> BV32 {
+    BV32::new(0x4567)
+}
+
+#[flux_rs::sig(fn () -> BV32{v: is_start(v)})]
+pub fn test3() -> BV32 {
+    BV32::new(0x4568) //~ ERROR: refinement type
+}
diff --git a/tests/tests/pos/surface/bitvec_const00.rs b/tests/tests/pos/surface/bitvec_const00.rs
@@ -0,0 +1,28 @@
+#![flux::defs(
+    fn is_start(x:bitvec<32>) -> bool { x == START }
+)]
+
+#[flux::opaque]
+#[flux::refined_by(val: bitvec<32>)]
+pub struct BV32(u32);
+
+impl BV32 {
+    #[flux::trusted]
+    #[flux::sig(fn (x:u32) -> BV32[bv_int_to_bv32(x)])]
+    const fn new(val: u32) -> Self {
+        BV32(val)
+    }
+}
+
+#[flux_rs::constant(bv_int_to_bv32(0x4567))]
+pub const START: BV32 = BV32::new(0x4567);
+
+#[flux_rs::sig(fn () -> BV32[START])]
+pub fn test1() -> BV32 {
+    BV32::new(0x4567)
+}
+
+#[flux_rs::sig(fn () -> BV32{v: is_start(v)})]
+pub fn test2() -> BV32 {
+    BV32::new(0x4567)
+}
diff --git a/tests/tests/todo/bitvec_const00.rs b/tests/tests/todo/bitvec_const00.rs
@@ -18,12 +18,11 @@ impl BV32 {
 pub const START: BV32 = BV32::new(0x4567);
 
 #[flux_rs::sig(fn () -> BV32[START])]
-fn test1() -> BV32 {
+pub fn test1() -> BV32 {
     BV32::new(0x4567)
 }
 
-// // USE: get the below to be SAFE
-// #[flux_rs::sig(fn () -> BV32{v: is_start(v)})]
-// fn test2() -> BV32 {
-//     BV32::new(0x4567)
-// }
+#[flux_rs::sig(fn () -> BV32{v: is_start(v)})]
+pub fn test2() -> BV32 {
+    BV32::new(0x4567)
+}