From ccc54a7061b135e9964fbb4f2e2b0f303b809edb Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Thu, 5 Dec 2024 14:25:55 -0800 Subject: [PATCH 1/4] Delay unfolding --- crates/flux-fhir-analysis/src/lib.rs | 32 +++++--------------------- crates/flux-infer/src/refine_tree.rs | 13 ++++++----- crates/flux-refineck/src/invariants.rs | 1 + crates/flux-refineck/src/lib.rs | 2 +- 4 files changed, 15 insertions(+), 33 deletions(-) diff --git a/crates/flux-fhir-analysis/src/lib.rs b/crates/flux-fhir-analysis/src/lib.rs index 3dedaeb8da..eeeae2af5f 100644 --- a/crates/flux-fhir-analysis/src/lib.rs +++ b/crates/flux-fhir-analysis/src/lib.rs @@ -119,7 +119,8 @@ fn qualifiers(genv: GlobalEnv) -> QueryResult> { .qualifiers() .map(|qualifier| { let wfckresults = wf::check_qualifier(genv, qualifier)?; - normalize(genv, conv::conv_qualifier(genv, qualifier, &wfckresults)?) + Ok(conv::conv_qualifier(genv, qualifier, &wfckresults)? + .normalize(genv.spec_func_defns()?)) }) .try_collect() } @@ -143,16 +144,7 @@ fn invariants_of(genv: GlobalEnv, item: &fhir::Item) -> QueryResult Err(query_bug!(item.owner_id.local_id(), "expected struct or enum"))?, }; let wfckresults = wf::check_invariants(genv, item.owner_id, params, invariants)?; - conv::conv_invariants( - genv, - item.owner_id.map(|it| it.def_id), - params, - invariants, - &wfckresults, - )? - .into_iter() - .map(|invariant| normalize(genv, invariant)) - .collect() + conv::conv_invariants(genv, item.owner_id.map(|it| it.def_id), params, invariants, &wfckresults) } fn predicates_of( @@ -487,23 +479,16 @@ fn variants_of( let wfckresults = genv.check_wf(local_id)?; let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt(); let variants = cx.conv_enum_variants(def_id, enum_def)?; - let variants = struct_compat::variants(genv, &variants, def_id)?; - let variants = variants - .into_iter() - .map(|variant| normalize(genv, variant)) - .try_collect()?; + let variants = rty::List::from_vec(struct_compat::variants(genv, &variants, def_id)?); rty::Opaqueness::Transparent(rty::EarlyBinder(variants)) } fhir::ItemKind::Struct(struct_def) => { let wfckresults = genv.check_wf(local_id)?; let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt(); cx.conv_struct_variant(def_id, struct_def)? - .map(|variant| { + .map(|variant| -> QueryResult<_> { let variants = struct_compat::variants(genv, &[variant], def_id)?; - variants - .into_iter() - .map(|variant| normalize(genv, variant)) - .try_collect() + Ok(rty::List::from_vec(variants)) }) .transpose()? .map(rty::EarlyBinder) @@ -528,7 +513,6 @@ fn fn_sig(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult Result<(), ErrorGuaranteed> { errors.into_result() } -fn normalize(genv: GlobalEnv, t: T) -> QueryResult { - Ok(t.normalize(genv.spec_func_defns()?)) -} - mod errors { use flux_errors::E0999; use flux_macros::Diagnostic; diff --git a/crates/flux-infer/src/refine_tree.rs b/crates/flux-infer/src/refine_tree.rs index c49f688cc0..d8b8a12bc2 100644 --- a/crates/flux-infer/src/refine_tree.rs +++ b/crates/flux-infer/src/refine_tree.rs @@ -234,8 +234,8 @@ impl RefineTree { Ok(RefineTree { root }) } - pub fn simplify(&mut self) { - self.root.borrow_mut().simplify(); + pub fn simplify(&mut self, genv: GlobalEnv) -> QueryResult { + self.root.borrow_mut().simplify(genv) } pub fn into_fixpoint(self, cx: &mut FixpointCtxt) -> QueryResult { @@ -415,14 +415,14 @@ impl std::ops::Deref for NodePtr { } impl Node { - fn simplify(&mut self) { + fn simplify(&mut self, genv: GlobalEnv) -> QueryResult { for child in &self.children { - child.borrow_mut().simplify(); + child.borrow_mut().simplify(genv)?; } match &mut self.kind { NodeKind::Head(pred, tag) => { - let pred = pred.simplify(); + let pred = pred.normalize(genv.spec_func_defns()?).simplify(); if pred.is_trivially_true() { self.kind = NodeKind::True; } else { @@ -431,7 +431,7 @@ impl Node { } NodeKind::True => {} NodeKind::Assumption(pred) => { - *pred = pred.simplify(); + *pred = pred.normalize(genv.spec_func_defns()?).simplify(); self.children .extract_if(|child| { matches!(child.borrow().kind, NodeKind::True) @@ -448,6 +448,7 @@ impl Node { if !self.is_leaf() && self.children.is_empty() { self.kind = NodeKind::True; } + Ok(()) } fn is_leaf(&self) -> bool { diff --git a/crates/flux-refineck/src/invariants.rs b/crates/flux-refineck/src/invariants.rs index 419aee6058..af011b46be 100644 --- a/crates/flux-refineck/src/invariants.rs +++ b/crates/flux-refineck/src/invariants.rs @@ -61,6 +61,7 @@ fn check_invariant( if config::dump_constraint() { dbg::dump_item_info(genv.tcx(), def_id.local_id(), "fluxc", &refine_tree).unwrap(); } + refine_tree.simplify(genv).emit(&genv)?; let cstr = refine_tree.into_fixpoint(&mut fcx).emit(&genv)?; let errors = fcx diff --git a/crates/flux-refineck/src/lib.rs b/crates/flux-refineck/src/lib.rs index dd49a98266..27e8bf34a0 100644 --- a/crates/flux-refineck/src/lib.rs +++ b/crates/flux-refineck/src/lib.rs @@ -89,7 +89,7 @@ fn invoke_fixpoint( if config::dump_constraint() { dbg::dump_item_info(genv.tcx(), local_id, ext, &refine_tree).unwrap(); } - refine_tree.simplify(); + refine_tree.simplify(genv).emit(&genv)?; let simp_ext = format!("simp.{}", ext); if config::dump_constraint() { dbg::dump_item_info(genv.tcx(), local_id, simp_ext, &refine_tree).unwrap(); From 66ee03603ff3b6516fa037e82e123b3dd532c2fa Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Fri, 6 Dec 2024 09:08:11 -0800 Subject: [PATCH 2/4] Move some stuff around --- crates/flux-infer/src/fixpoint_encoding.rs | 11 ++++--- crates/flux-infer/src/refine_tree.rs | 17 +++++------ crates/flux-middle/src/rty/expr.rs | 13 +++++--- crates/flux-refineck/src/checker.rs | 2 +- crates/flux-refineck/src/invariants.rs | 24 +++++++-------- crates/flux-refineck/src/lib.rs | 32 ++++++++++---------- tests/tests/neg/error_messages/localize02.rs | 4 +-- 7 files changed, 55 insertions(+), 48 deletions(-) diff --git a/crates/flux-infer/src/fixpoint_encoding.rs b/crates/flux-infer/src/fixpoint_encoding.rs index cee4682130..52f46bcfc5 100644 --- a/crates/flux-infer/src/fixpoint_encoding.rs +++ b/crates/flux-infer/src/fixpoint_encoding.rs @@ -19,6 +19,7 @@ use flux_middle::{ global_env::GlobalEnv, queries::QueryResult, rty::{self, BoundVariableKind, ESpan, Lambda, List}, + MaybeExternId, }; use itertools::Itertools; use liquid_fixpoint::FixpointResult; @@ -320,7 +321,7 @@ pub struct FixpointCtxt<'genv, 'tcx, T: Eq + Hash> { tags_inv: UnordMap, /// [`DefId`] of the item being checked. This can be a function/method or an adt when checking /// invariants. - def_id: LocalDefId, + def_id: MaybeExternId, } pub type FixQueryCache = QueryCache>; @@ -329,7 +330,7 @@ impl<'genv, 'tcx, Tag> FixpointCtxt<'genv, 'tcx, Tag> where Tag: std::hash::Hash + Eq + Copy, { - pub fn new(genv: GlobalEnv<'genv, 'tcx>, def_id: LocalDefId, kvars: KVarGen) -> Self { + pub fn new(genv: GlobalEnv<'genv, 'tcx>, def_id: MaybeExternId, kvars: KVarGen) -> Self { let def_span = genv.tcx().def_span(def_id); Self { comments: vec![], @@ -361,7 +362,9 @@ where let constraint = self.ecx.assume_const_values(constraint); - let qualifiers = self.ecx.qualifiers_for(self.def_id, &mut self.scx)?; + let qualifiers = self + .ecx + .qualifiers_for(self.def_id.local_id(), &mut self.scx)?; let mut constants = self .ecx @@ -397,7 +400,7 @@ where data_decls: self.scx.into_data_decls(), }; if config::dump_constraint() { - dbg::dump_item_info(self.genv.tcx(), self.def_id, "smt2", &task).unwrap(); + dbg::dump_item_info(self.genv.tcx(), self.def_id.resolved_id(), "smt2", &task).unwrap(); } let task_key = self.genv.tcx().def_path_str(self.def_id); diff --git a/crates/flux-infer/src/refine_tree.rs b/crates/flux-infer/src/refine_tree.rs index d8b8a12bc2..c6e6b4da13 100644 --- a/crates/flux-infer/src/refine_tree.rs +++ b/crates/flux-infer/src/refine_tree.rs @@ -14,8 +14,8 @@ use flux_middle::{ canonicalize::{Hoister, HoisterDelegate}, evars::EVarSol, fold::{TypeFoldable, TypeSuperVisitable, TypeVisitable, TypeVisitor}, - BaseTy, EarlyBinder, EarlyReftParam, Expr, GenericArgs, Name, Sort, Ty, TyCtor, TyKind, - Var, + BaseTy, EarlyBinder, EarlyReftParam, Expr, GenericArgs, Name, Sort, SpecFuncDefns, Ty, + TyCtor, TyKind, Var, }, }; use itertools::Itertools; @@ -234,8 +234,8 @@ impl RefineTree { Ok(RefineTree { root }) } - pub fn simplify(&mut self, genv: GlobalEnv) -> QueryResult { - self.root.borrow_mut().simplify(genv) + pub fn simplify(&mut self, defns: &SpecFuncDefns) { + self.root.borrow_mut().simplify(defns) } pub fn into_fixpoint(self, cx: &mut FixpointCtxt) -> QueryResult { @@ -415,14 +415,14 @@ impl std::ops::Deref for NodePtr { } impl Node { - fn simplify(&mut self, genv: GlobalEnv) -> QueryResult { + fn simplify(&mut self, defns: &SpecFuncDefns) { for child in &self.children { - child.borrow_mut().simplify(genv)?; + child.borrow_mut().simplify(defns); } match &mut self.kind { NodeKind::Head(pred, tag) => { - let pred = pred.normalize(genv.spec_func_defns()?).simplify(); + let pred = pred.normalize(defns).simplify(); if pred.is_trivially_true() { self.kind = NodeKind::True; } else { @@ -431,7 +431,7 @@ impl Node { } NodeKind::True => {} NodeKind::Assumption(pred) => { - *pred = pred.normalize(genv.spec_func_defns()?).simplify(); + *pred = pred.normalize(defns).simplify(); self.children .extract_if(|child| { matches!(child.borrow().kind, NodeKind::True) @@ -448,7 +448,6 @@ impl Node { if !self.is_leaf() && self.children.is_empty() { self.kind = NodeKind::True; } - Ok(()) } fn is_leaf(&self) -> bool { diff --git a/crates/flux-middle/src/rty/expr.rs b/crates/flux-middle/src/rty/expr.rs index 4cbbe65a82..513b10563b 100644 --- a/crates/flux-middle/src/rty/expr.rs +++ b/crates/flux-middle/src/rty/expr.rs @@ -119,7 +119,9 @@ impl ESpan { } } -#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeFoldable, TypeVisitable)] +#[derive( + Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeFoldable, TypeVisitable, +)] pub enum BinOp { Iff, Imp, @@ -1144,6 +1146,7 @@ mod pretty { } } let e = if cx.simplify_exprs { self.simplify() } else { self.clone() }; + // w!("{:?}@(", ^e.span())?; match e.kind() { ExprKind::Var(var) => w!("{:?}", var), ExprKind::Local(local) => w!("{:?}", ^local), @@ -1221,8 +1224,8 @@ mod pretty { } } ExprKind::App(func, args) => { - w!("({:?})({})", - func, + w!("{:?}({})", + parens!(func, !func.is_atom()), ^args .iter() .format_with(", ", |arg, f| f(&format_args_cx!("{:?}", arg))) @@ -1253,7 +1256,9 @@ mod pretty { w!("{:?}", expr.as_ref().skip_binder()) }) } - } + }?; + // w!(")") + Ok(()) } } diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 49e4a2494e..6f63acae99 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -1950,7 +1950,7 @@ pub(crate) mod errors { Self { kind: CheckerErrKind::OpaqueStruct(def_id), span } } - pub fn emit_err(self, genv: &GlobalEnv, fn_def_id: MaybeExternId) -> ErrorGuaranteed { + pub fn emit(self, genv: GlobalEnv, fn_def_id: MaybeExternId) -> ErrorGuaranteed { let dcx = genv.sess().dcx().handle(); match self.kind { CheckerErrKind::Inference => { diff --git a/crates/flux-refineck/src/invariants.rs b/crates/flux-refineck/src/invariants.rs index af011b46be..be5553b37b 100644 --- a/crates/flux-refineck/src/invariants.rs +++ b/crates/flux-refineck/src/invariants.rs @@ -1,5 +1,4 @@ -use flux_common::{dbg, iter::IterExt, result::ResultExt}; -use flux_config as config; +use flux_common::{cache::QueryCache, iter::IterExt, result::ResultExt}; use flux_errors::ErrorGuaranteed; use flux_infer::{ fixpoint_encoding::{FixQueryCache, FixpointCtxt, KVarGen}, @@ -9,7 +8,7 @@ use flux_infer::{ use flux_middle::{fhir, global_env::GlobalEnv, rty, MaybeExternId}; use rustc_span::{Span, DUMMY_SP}; -use crate::CheckerConfig; +use crate::{invoke_fixpoint, CheckerConfig}; pub fn check_invariants( genv: GlobalEnv, @@ -57,16 +56,17 @@ fn check_invariant( let pred = invariant.apply(&variant.idx); rcx.check_pred(&pred, Tag::new(ConstrReason::Other, DUMMY_SP)); } - let mut fcx = FixpointCtxt::new(genv, def_id.local_id(), KVarGen::dummy()); - if config::dump_constraint() { - dbg::dump_item_info(genv.tcx(), def_id.local_id(), "fluxc", &refine_tree).unwrap(); - } - refine_tree.simplify(genv).emit(&genv)?; + let errors = invoke_fixpoint( + genv, + cache, + def_id, + refine_tree, + KVarGen::dummy(), + checker_config, + "fluxc", + ) + .emit(&genv)?; - let cstr = refine_tree.into_fixpoint(&mut fcx).emit(&genv)?; - let errors = fcx - .check(cache, cstr, checker_config.scrape_quals) - .emit(&genv)?; if errors.is_empty() { Ok(()) } else { diff --git a/crates/flux-refineck/src/lib.rs b/crates/flux-refineck/src/lib.rs index 27e8bf34a0..aa0e4d48c7 100644 --- a/crates/flux-refineck/src/lib.rs +++ b/crates/flux-refineck/src/lib.rs @@ -80,24 +80,24 @@ fn report_fixpoint_errors( fn invoke_fixpoint( genv: GlobalEnv, cache: &mut FixQueryCache, - local_id: LocalDefId, + def_id: MaybeExternId, mut refine_tree: RefineTree, kvars: KVarGen, config: CheckerConfig, ext: &str, -) -> Result, ErrorGuaranteed> { +) -> QueryResult> { if config::dump_constraint() { - dbg::dump_item_info(genv.tcx(), local_id, ext, &refine_tree).unwrap(); + dbg::dump_item_info(genv.tcx(), def_id.resolved_id(), ext, &refine_tree).unwrap(); } - refine_tree.simplify(genv).emit(&genv)?; + refine_tree.simplify(genv.spec_func_defns()?); let simp_ext = format!("simp.{}", ext); if config::dump_constraint() { - dbg::dump_item_info(genv.tcx(), local_id, simp_ext, &refine_tree).unwrap(); + dbg::dump_item_info(genv.tcx(), def_id.resolved_id(), simp_ext, &refine_tree).unwrap(); } - let mut fcx = FixpointCtxt::new(genv, local_id, kvars); - let cstr = refine_tree.into_fixpoint(&mut fcx).emit(&genv)?; - fcx.check(cache, cstr, config.scrape_quals).emit(&genv) + let mut fcx = FixpointCtxt::new(genv, def_id, kvars); + let cstr = refine_tree.into_fixpoint(&mut fcx)?; + fcx.check(cache, cstr, config.scrape_quals) } pub fn check_fn( @@ -147,34 +147,34 @@ pub fn check_fn( dbg::check_fn_span!(genv.tcx(), local_id).in_scope(|| { let ghost_stmts = compute_ghost_statements(genv, local_id) .with_span(span) - .map_err(|err| err.emit_err(&genv, def_id))?; + .map_err(|err| err.emit(genv, def_id))?; // PHASE 1: infer shape of `TypeEnv` at the entry of join points let shape_result = Checker::run_in_shape_mode(genv, local_id, &ghost_stmts, config) - // Augment the possible CheckError with the functions span so we can report - // helpful error messages for opaque struct field accesses - .map_err(|err| err.emit_err(&genv, def_id))?; + .map_err(|err| err.emit(genv, def_id))?; tracing::info!("check_fn::shape"); // PHASE 2: generate refinement tree constraint let (refine_tree, kvars) = Checker::run_in_refine_mode(genv, local_id, &ghost_stmts, shape_result, config) - .map_err(|err| err.emit_err(&genv, def_id))?; + .map_err(|err| err.emit(genv, def_id))?; tracing::info!("check_fn::refine"); // PHASE 3: invoke fixpoint on the constraint - let errors = invoke_fixpoint(genv, cache, local_id, refine_tree, kvars, config, "fluxc")?; + let errors = invoke_fixpoint(genv, cache, def_id, refine_tree, kvars, config, "fluxc") + .emit(&genv)?; tracing::info!("check_fn::fixpoint"); report_fixpoint_errors(genv, local_id, errors)?; // PHASE 4: subtyping check for trait-method implementations if let Some((refine_tree, kvars)) = trait_impl_subtyping(genv, local_id, config.check_overflow, span) - .map_err(|err| err.emit_err(&genv, def_id))? + .map_err(|err| err.emit(genv, def_id))? { tracing::info!("check_fn::refine-subtyping"); let errors = - invoke_fixpoint(genv, cache, local_id, refine_tree, kvars, config, "sub.fluxc")?; + invoke_fixpoint(genv, cache, def_id, refine_tree, kvars, config, "sub.fluxc") + .emit(&genv)?; tracing::info!("check_fn::fixpoint-subtyping"); report_fixpoint_errors(genv, local_id, errors)?; } diff --git a/tests/tests/neg/error_messages/localize02.rs b/tests/tests/neg/error_messages/localize02.rs index 8db8f77391..3ffd5357e0 100644 --- a/tests/tests/neg/error_messages/localize02.rs +++ b/tests/tests/neg/error_messages/localize02.rs @@ -9,7 +9,7 @@ } fn inc1(x: int) -> int { - x + 1 //~ NOTE this is the condition + x + 1 } }] @@ -21,7 +21,7 @@ fn test() { //~| NOTE a precondition cannot be proved } -#[flux::sig(fn() -> i32[inc1(0)])] //~ NOTE inside this call +#[flux::sig(fn() -> i32[inc1(0)])] //~ NOTE this is the condition fn moo() -> i32 { 2 //~ ERROR refinement type //~| NOTE a postcondition cannot be proved From e9908a5b1e7d2361002a6eadd0b9eb4460320d08 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Fri, 6 Dec 2024 09:08:37 -0800 Subject: [PATCH 3/4] ASdf --- crates/flux-infer/src/refine_tree.rs | 2 +- crates/flux-refineck/src/invariants.rs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/crates/flux-infer/src/refine_tree.rs b/crates/flux-infer/src/refine_tree.rs index c6e6b4da13..f6295ff065 100644 --- a/crates/flux-infer/src/refine_tree.rs +++ b/crates/flux-infer/src/refine_tree.rs @@ -235,7 +235,7 @@ impl RefineTree { } pub fn simplify(&mut self, defns: &SpecFuncDefns) { - self.root.borrow_mut().simplify(defns) + self.root.borrow_mut().simplify(defns); } pub fn into_fixpoint(self, cx: &mut FixpointCtxt) -> QueryResult { diff --git a/crates/flux-refineck/src/invariants.rs b/crates/flux-refineck/src/invariants.rs index be5553b37b..bc11b6f86f 100644 --- a/crates/flux-refineck/src/invariants.rs +++ b/crates/flux-refineck/src/invariants.rs @@ -1,7 +1,7 @@ -use flux_common::{cache::QueryCache, iter::IterExt, result::ResultExt}; +use flux_common::{iter::IterExt, result::ResultExt}; use flux_errors::ErrorGuaranteed; use flux_infer::{ - fixpoint_encoding::{FixQueryCache, FixpointCtxt, KVarGen}, + fixpoint_encoding::{FixQueryCache, KVarGen}, infer::{ConstrReason, Tag}, refine_tree::RefineTree, }; From c545c46296539db6234552df12a635730da2d1ec Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Fri, 6 Dec 2024 09:49:13 -0800 Subject: [PATCH 4/4] ups --- crates/flux-middle/src/rty/expr.rs | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/crates/flux-middle/src/rty/expr.rs b/crates/flux-middle/src/rty/expr.rs index 513b10563b..7f2d464bfb 100644 --- a/crates/flux-middle/src/rty/expr.rs +++ b/crates/flux-middle/src/rty/expr.rs @@ -119,9 +119,7 @@ impl ESpan { } } -#[derive( - Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeFoldable, TypeVisitable, -)] +#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeFoldable, TypeVisitable)] pub enum BinOp { Iff, Imp, @@ -1146,7 +1144,6 @@ mod pretty { } } let e = if cx.simplify_exprs { self.simplify() } else { self.clone() }; - // w!("{:?}@(", ^e.span())?; match e.kind() { ExprKind::Var(var) => w!("{:?}", var), ExprKind::Local(local) => w!("{:?}", ^local), @@ -1256,9 +1253,7 @@ mod pretty { w!("{:?}", expr.as_ref().skip_binder()) }) } - }?; - // w!(")") - Ok(()) + } } }