From 180bde55b49c2b3e27ebb49e90073234bcab2e50 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Wed, 11 Dec 2024 20:25:30 -0800 Subject: [PATCH] tests pass? --- crates/flux-desugar/src/desugar.rs | 4 +-- crates/flux-fhir-analysis/src/conv/mod.rs | 16 +++++++++-- crates/flux-fhir-analysis/src/lib.rs | 4 ++- crates/flux-fhir-analysis/src/wf/mod.rs | 21 +++++++++++++- crates/flux-fhir-analysis/src/wf/sortck.rs | 15 +++------- crates/flux-infer/src/fixpoint_encoding.rs | 3 +- crates/flux-middle/src/fhir.rs | 8 ++++++ crates/flux-middle/src/queries.rs | 7 ++--- crates/flux-middle/src/rty/mod.rs | 4 +-- crates/flux-middle/src/sort_of.rs | 9 ++++++ tests/tests/neg/surface/bitvec_const00.rs | 33 ++++++++++++++++++++++ tests/tests/pos/surface/bitvec_const00.rs | 28 ++++++++++++++++++ tests/tests/todo/bitvec_const00.rs | 11 ++++---- 13 files changed, 132 insertions(+), 31 deletions(-) create mode 100644 tests/tests/neg/surface/bitvec_const00.rs create mode 100644 tests/tests/pos/surface/bitvec_const00.rs diff --git a/crates/flux-desugar/src/desugar.rs b/crates/flux-desugar/src/desugar.rs index 6f735f22c0..30be44654e 100644 --- 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 index 6e97679990..aa0f91c3a5 100644 --- 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 { + 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

{ pub(crate) fn conv_constant_info( &mut self, - def_id: MaybeExternId, constant_info: &fhir::ConstantInfo, ) -> QueryResult { - 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 index 8cf0d9ce84..0fdfed2d08 100644 --- 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 { fn constant_info(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult { 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> { diff --git a/crates/flux-fhir-analysis/src/wf/mod.rs b/crates/flux-fhir-analysis/src/wf/mod.rs index e4dd104a4c..8da773e9d0 100644 --- 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, + constant: &fhir::ConstantInfo, +) -> Result { + 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, @@ -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 index d72ad310c1..4964276fb1 100644 --- 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 index 207f2b0360..f83897f15e 100644 --- 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 index 78618364ae..e175cdd3f2 100644 --- 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 index 5eb35b5f56..93cb150ade 100644 --- 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 index 48315082d0..2a6e3fbc35 100644 --- 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, } diff --git a/crates/flux-middle/src/sort_of.rs b/crates/flux-middle/src/sort_of.rs index 19beaf54f5..494464f343 100644 --- 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> { + 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 new file mode 100644 index 0000000000..0cdc2513e8 --- /dev/null +++ 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 new file mode 100644 index 0000000000..b2b6b34882 --- /dev/null +++ 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 index 8ccbaec9fb..b2b6b34882 100644 --- 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) +}