From 5bfa567b43c1ead524c38afe1abf220c8486e089 Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Thu, 7 Nov 2024 14:29:05 -0800 Subject: [PATCH 01/15] Add constructors without spreads --- crates/flux-desugar/locales/en-US.ftl | 3 + crates/flux-desugar/src/desugar.rs | 36 ++++++++++ crates/flux-desugar/src/errors.rs | 7 ++ .../src/resolver/refinement_resolver.rs | 20 ++++-- crates/flux-fhir-analysis/locales/en-US.ftl | 4 ++ crates/flux-fhir-analysis/src/conv/mod.rs | 37 +++++++++- crates/flux-fhir-analysis/src/wf/errors.rs | 14 ++++ .../flux-fhir-analysis/src/wf/param_usage.rs | 5 ++ crates/flux-fhir-analysis/src/wf/sortck.rs | 42 +++++++++++ crates/flux-middle/src/fhir.rs | 27 +++++++ crates/flux-middle/src/fhir/visit.rs | 25 +++++-- crates/flux-middle/src/rty/mod.rs | 4 ++ crates/flux-syntax/src/grammar.lalrpop | 70 +++++++++++++------ crates/flux-syntax/src/lexer.rs | 1 + crates/flux-syntax/src/surface.rs | 16 +++++ crates/flux-syntax/src/surface/visit.rs | 24 +++++-- 16 files changed, 301 insertions(+), 34 deletions(-) diff --git a/crates/flux-desugar/locales/en-US.ftl b/crates/flux-desugar/locales/en-US.ftl index bd4e4b1fa0..a3b66f2beb 100644 --- a/crates/flux-desugar/locales/en-US.ftl +++ b/crates/flux-desugar/locales/en-US.ftl @@ -13,6 +13,9 @@ desugar_unexpected_literal = desugar_invalid_dot_var = unsupported field access in refinement +desugar_invalid_constructor_path = + invalid use of path in constructor + desugar_invalid_func_as_var = invalid use of function .label = function not supported in this position diff --git a/crates/flux-desugar/src/desugar.rs b/crates/flux-desugar/src/desugar.rs index f45fb2e948..aa9dd5f828 100644 --- a/crates/flux-desugar/src/desugar.rs +++ b/crates/flux-desugar/src/desugar.rs @@ -1389,11 +1389,47 @@ trait DesugarCtxt<'genv, 'tcx: 'genv> { self.genv().alloc(e2?), ) } + surface::ExprKind::Constructor(path, constructor_args, spread) => { + let path = self.desugar_constructor_path(path)?; + let constructor_args = + try_alloc_slice!(self.genv(), constructor_args, |field_expr| { + let e = self.desugar_expr(&field_expr.expr)?; + Ok(fhir::FieldExpr { + ident: field_expr.ident, + expr: e, + fhir_id: self.next_fhir_id(), + span: e.span, + }) + })?; + let spread = match spread { + None => None, + Some(s) => { + Some(fhir::Spread { + path: self.desugar_constructor_path(&s.path)?, + span: s.span, + fhir_id: self.next_fhir_id(), + }) + } + }; + fhir::ExprKind::Constructor(path, constructor_args, spread) + } }; Ok(fhir::Expr { kind, span: expr.span, fhir_id: self.next_fhir_id() }) } + fn desugar_constructor_path(&self, path: &surface::ExprPath) -> Result> { + let res = self.resolver_output().expr_path_res_map[&path.node_id]; + if let ExprRes::Struct(..) | ExprRes::Enum(..) = res { + let segments = self + .genv() + .alloc_slice_fill_iter(path.segments.iter().map(|s| s.ident)); + Ok(fhir::PathExpr { segments, res, fhir_id: self.next_fhir_id(), span: path.span }) + } else { + Err(self.emit_err(errors::InvalidConstructorPath { span: path.span })) + } + } + fn desugar_exprs(&mut self, exprs: &[surface::Expr]) -> Result<&'genv [fhir::Expr<'genv>]> { try_alloc_slice!(self.genv(), exprs, |e| self.desugar_expr(e)) } diff --git a/crates/flux-desugar/src/errors.rs b/crates/flux-desugar/src/errors.rs index f01e17b0cb..f8e9158d11 100644 --- a/crates/flux-desugar/src/errors.rs +++ b/crates/flux-desugar/src/errors.rs @@ -17,6 +17,13 @@ pub(super) struct UnexpectedLiteral { pub(super) span: Span, } +#[derive(Diagnostic)] +#[diag(desugar_invalid_constructor_path, code = E0999)] +pub(super) struct InvalidConstructorPath { + #[primary_span] + pub(super) span: Span, +} + #[derive(Diagnostic)] #[diag(desugar_invalid_dot_var, code = E0999)] pub(super) struct InvalidDotVar { diff --git a/crates/flux-desugar/src/resolver/refinement_resolver.rs b/crates/flux-desugar/src/resolver/refinement_resolver.rs index 59f9e1d712..3f01a3d33b 100644 --- a/crates/flux-desugar/src/resolver/refinement_resolver.rs +++ b/crates/flux-desugar/src/resolver/refinement_resolver.rs @@ -296,6 +296,12 @@ impl surface::visit::Visitor for ScopedVisitorWrapper { self.on_func(*func, expr.node_id); } surface::ExprKind::Dot(path, _) => self.on_path(path), + surface::ExprKind::Constructor(path, _, spread) => { + self.on_path(path); + if let Some(s) = spread { + self.on_path(&s.path); + } + } _ => {} } surface::visit::walk_expr(self, expr); @@ -556,13 +562,19 @@ impl<'a, 'genv, 'tcx> RefinementResolver<'a, 'genv, 'tcx> { &mut self, segments: &[S], ) -> Option> { - let res = self - .resolver - .resolve_path_with_ribs(segments, ValueNS)? - .full_res()?; + let res = match self.resolver.resolve_path_with_ribs(segments, ValueNS) { + Some(r) => r.full_res()?, + _ => { + self.resolver + .resolve_path_with_ribs(segments, TypeNS)? + .full_res()? + } + }; match res { fhir::Res::Def(DefKind::ConstParam, def_id) => Some(ExprRes::ConstGeneric(def_id)), fhir::Res::Def(DefKind::Const, def_id) => Some(ExprRes::Const(def_id)), + fhir::Res::Def(DefKind::Struct, def_id) => Some(ExprRes::Struct(def_id)), + fhir::Res::Def(DefKind::Enum, def_id) => Some(ExprRes::Enum(def_id)), _ => None, } } diff --git a/crates/flux-fhir-analysis/locales/en-US.ftl b/crates/flux-fhir-analysis/locales/en-US.ftl index 0f3b941bcc..ce8a2db2c3 100644 --- a/crates/flux-fhir-analysis/locales/en-US.ftl +++ b/crates/flux-fhir-analysis/locales/en-US.ftl @@ -66,6 +66,10 @@ fhir_analysis_param_count_mismatch = *[other] {$expected} parameters } was expected +fhir_analysis_invalid_field_update = + invalid field referenced in constructor + .label = field does not exist + fhir_analysis_field_not_found = no field `{$fld}` on sort `{$sort}` diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 08ecb9641b..2fb969353a 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -48,7 +48,7 @@ use rustc_target::spec::abi; use rustc_trait_selection::traits; use rustc_type_ir::DebruijnIndex; -use crate::compare_impl_item::errors::InvalidAssocReft; +use crate::{adt_sort_def_of, compare_impl_item::errors::InvalidAssocReft}; pub struct ConvCtxt<'genv, 'tcx, P> { genv: GlobalEnv<'genv, 'tcx>, @@ -1566,6 +1566,8 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, P> { ExprRes::GlobalFunc(..) => { span_bug!(var.span, "unexpected func in var position") } + ExprRes::Struct(..) => span_bug!(var.span, "unexpected struct in var position"), + ExprRes::Enum(..) => span_bug!(var.span, "unexpected enum in var position"), } } fhir::ExprKind::Literal(lit) => rty::Expr::constant(conv_lit(*lit)).at(espan), @@ -1620,10 +1622,43 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, P> { .try_collect()?; rty::Expr::adt(def_id, flds) } + fhir::ExprKind::Constructor(path, exprs, spread) => { + let def_id = match path.res { + ExprRes::Struct(def_id) | ExprRes::Enum(def_id) => def_id, + _ => span_bug!(path.span, "unexpected path in constructor"), + }; + let assns = self.conv_constructor_exprs(def_id, env, exprs, spread)?; + rty::Expr::adt(def_id, assns) + } }; Ok(self.add_coercions(expr, fhir_id)) } + fn conv_constructor_exprs( + &mut self, + struct_def_id: DefId, + env: &mut Env, + exprs: &[fhir::FieldExpr], + _spread: &Option, + ) -> QueryResult> { + if let Some(local_def_id) = struct_def_id.as_local() { + let struct_adt = adt_sort_def_of(self.genv, local_def_id)?; + let field_names = struct_adt.field_names(); + let mut assns = Vec::new(); + for expr_val in exprs { + let field_symbol = expr_val.ident.name; + let pos = field_names.iter().position(|s| *s == field_symbol); + if let Some(idx) = pos { + assns.push((self.conv_expr(env, &expr_val.expr)?, idx)) + } + } + assns.sort_by(|lhs, rhs| lhs.1.cmp(&rhs.1)); + Ok(assns.into_iter().map(|x| x.0).collect()) + } else { + todo!() + } + } + fn conv_exprs(&mut self, env: &mut Env, exprs: &[fhir::Expr]) -> QueryResult> { exprs.iter().map(|e| self.conv_expr(env, e)).collect() } diff --git a/crates/flux-fhir-analysis/src/wf/errors.rs b/crates/flux-fhir-analysis/src/wf/errors.rs index 41d8179e8a..532e08c459 100644 --- a/crates/flux-fhir-analysis/src/wf/errors.rs +++ b/crates/flux-fhir-analysis/src/wf/errors.rs @@ -137,6 +137,20 @@ impl<'a> UnexpectedFun<'a> { } } +#[derive(Diagnostic)] +#[diag(fhir_analysis_invalid_field_update, code = E0999)] +pub(super) struct InvalidFieldUpdate { + #[primary_span] + #[label] + span: Span, +} + +impl InvalidFieldUpdate { + pub(super) fn new(span: Span) -> Self { + Self { span } + } +} + #[derive(Diagnostic)] #[diag(fhir_analysis_param_count_mismatch, code = E0999)] pub(super) struct ParamCountMismatch { diff --git a/crates/flux-fhir-analysis/src/wf/param_usage.rs b/crates/flux-fhir-analysis/src/wf/param_usage.rs index b38ea52a29..bd3fb513ba 100644 --- a/crates/flux-fhir-analysis/src/wf/param_usage.rs +++ b/crates/flux-fhir-analysis/src/wf/param_usage.rs @@ -118,6 +118,11 @@ impl<'a, 'genv, 'tcx> ParamUsesChecker<'a, 'genv, 'tcx> { self.check_func_params_uses(field, is_top_level_conj, is_top_level_var); } } + fhir::ExprKind::Constructor(_path, exprs, _spread) => { + for expr in exprs { + self.check_func_params_uses(&expr.expr, is_top_level_conj, is_top_level_var); + } + } } } diff --git a/crates/flux-fhir-analysis/src/wf/sortck.rs b/crates/flux-fhir-analysis/src/wf/sortck.rs index 3ccd6fc4e7..fa2a9b803d 100644 --- a/crates/flux-fhir-analysis/src/wf/sortck.rs +++ b/crates/flux-fhir-analysis/src/wf/sortck.rs @@ -84,6 +84,39 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { } } + fn check_constructor( + &mut self, + path: &fhir::PathExpr, + field_exprs: &[fhir::FieldExpr], + _spread: &Option, + expected: &rty::Sort, + ) -> Result { + if let rty::Sort::App(rty::SortCtor::Adt(sort_def), sort_args) = expected { + // these are ordered + let field_names = sort_def.field_names(); + let sorts = sort_def.field_sorts(sort_args); + for expr in field_exprs { + // make sure that the field is actually a field + if let Some(idx) = field_names.iter().position(|s| *s == expr.ident.name) { + // check that field sort is the same as the expr sort + let sort = &sorts[idx]; + self.check_expr(&expr.expr, sort)? + } else { + // emit an error because we have a mismatched field + return Err(self.emit_err(errors::InvalidFieldUpdate::new(expr.ident.span))); + } + } + Ok(()) + } else { + Err(self.emit_err(errors::ArgCountMismatch::new( + Some(path.span), + String::from("type"), + 1, + field_exprs.len(), + ))) + } + } + fn check_record( &mut self, arg: &fhir::Expr, @@ -142,6 +175,9 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { self.check_abs(expr, refine_params, body, expected)? } fhir::ExprKind::Record(fields) => self.check_record(expr, fields, expected)?, + fhir::ExprKind::Constructor(path, exprs, spread) => { + self.check_constructor(path, exprs, spread, expected)? + } } Ok(()) } @@ -210,6 +246,12 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { ExprRes::GlobalFunc(_, _) => { span_bug!(path.span, "unexpected func in var position") } + ExprRes::Struct(_) => { + span_bug!(path.span, "unexpected struct in var position") + } + ExprRes::Enum(_) => { + span_bug!(path.span, "unexpected enum in var position") + } } } diff --git a/crates/flux-middle/src/fhir.rs b/crates/flux-middle/src/fhir.rs index 4bab1914e7..901c48ba19 100644 --- a/crates/flux-middle/src/fhir.rs +++ b/crates/flux-middle/src/fhir.rs @@ -901,6 +901,21 @@ pub struct AliasReft<'fhir> { pub name: Symbol, } +#[derive(Debug, Clone, Copy)] +pub struct FieldExpr<'fhir> { + pub ident: Ident, + pub expr: Expr<'fhir>, + pub fhir_id: FhirId, + pub span: Span, +} + +#[derive(Debug, Clone, Copy)] +pub struct Spread<'fhir> { + pub path: PathExpr<'fhir>, + pub span: Span, + pub fhir_id: FhirId, +} + #[derive(Clone, Copy)] pub struct Expr<'fhir> { pub kind: ExprKind<'fhir>, @@ -920,6 +935,7 @@ pub enum ExprKind<'fhir> { IfThenElse(&'fhir Expr<'fhir>, &'fhir Expr<'fhir>, &'fhir Expr<'fhir>), Abs(&'fhir [RefineParam<'fhir>], &'fhir Expr<'fhir>), Record(&'fhir [Expr<'fhir>]), + Constructor(PathExpr<'fhir>, &'fhir [FieldExpr<'fhir>], Option>), } impl<'fhir> Expr<'fhir> { @@ -947,6 +963,8 @@ pub enum Lit { pub enum ExprRes { Param(ParamKind, Id), Const(DefId), + Struct(DefId), + Enum(DefId), ConstGeneric(DefId), NumConst(i128), GlobalFunc(SpecFuncKind, Symbol), @@ -960,6 +978,8 @@ impl ExprRes { ExprRes::NumConst(val) => ExprRes::NumConst(val), ExprRes::GlobalFunc(kind, name) => ExprRes::GlobalFunc(kind, name), ExprRes::ConstGeneric(def_id) => ExprRes::ConstGeneric(def_id), + ExprRes::Struct(def_id) => ExprRes::Struct(def_id), + ExprRes::Enum(def_id) => ExprRes::Enum(def_id), } } @@ -1429,6 +1449,13 @@ impl fmt::Debug for Expr<'_> { ExprKind::Record(flds) => { write!(f, "{{ {:?} }}", flds.iter().format(", ")) } + ExprKind::Constructor(path, exprs, spread) => { + if let Some(s) = spread { + write!(f, "{:?} {{ {:?}, ..{:?} }}", path, exprs.iter().format(", "), s) + } else { + write!(f, "{:?} {{ {:?} }}", path, exprs.iter().format(", ")) + } + } } } } diff --git a/crates/flux-middle/src/fhir/visit.rs b/crates/flux-middle/src/fhir/visit.rs index 26ed44bd70..6371e3e1a0 100644 --- a/crates/flux-middle/src/fhir/visit.rs +++ b/crates/flux-middle/src/fhir/visit.rs @@ -1,10 +1,10 @@ use super::{ AliasReft, AssocItemConstraint, AssocItemConstraintKind, BaseTy, BaseTyKind, Ensures, EnumDef, - Expr, ExprKind, FieldDef, FnDecl, FnOutput, FnSig, FuncSort, GenericArg, GenericBound, - Generics, Impl, ImplAssocReft, ImplItem, ImplItemKind, Item, ItemKind, Lifetime, Lit, Node, - OpaqueTy, Path, PathExpr, PathSegment, PolyFuncSort, PolyTraitRef, QPath, RefineParam, - Requires, Sort, SortPath, StructDef, TraitAssocReft, TraitItem, TraitItemKind, Ty, TyAlias, - TyKind, VariantDef, VariantRet, WhereBoundPredicate, + Expr, ExprKind, FieldDef, FieldExpr, FnDecl, FnOutput, FnSig, FuncSort, GenericArg, + GenericBound, Generics, Impl, ImplAssocReft, ImplItem, ImplItemKind, Item, ItemKind, Lifetime, + Lit, Node, OpaqueTy, Path, PathExpr, PathSegment, PolyFuncSort, PolyTraitRef, QPath, + RefineParam, Requires, Sort, SortPath, StructDef, TraitAssocReft, TraitItem, TraitItemKind, Ty, + TyAlias, TyKind, VariantDef, VariantRet, WhereBoundPredicate, }; use crate::fhir::StructKind; @@ -167,6 +167,10 @@ pub trait Visitor<'v>: Sized { walk_expr(self, expr); } + fn visit_field_expr(&mut self, expr: &FieldExpr<'v>) { + walk_field_expr(self, expr); + } + fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'v>) { walk_alias_reft(self, alias_reft); } @@ -453,6 +457,10 @@ pub fn walk_alias_reft<'v, V: Visitor<'v>>(vis: &mut V, alias: &AliasReft<'v>) { vis.visit_path(&alias.path); } +pub fn walk_field_expr<'v, V: Visitor<'v>>(vis: &mut V, expr: &FieldExpr<'v>) { + vis.visit_expr(&expr.expr); +} + pub fn walk_expr<'v, V: Visitor<'v>>(vis: &mut V, expr: &Expr<'v>) { match expr.kind { ExprKind::Var(path, _) => vis.visit_path_expr(&path), @@ -484,5 +492,12 @@ pub fn walk_expr<'v, V: Visitor<'v>>(vis: &mut V, expr: &Expr<'v>) { ExprKind::Record(fields) => { walk_list!(vis, visit_expr, fields); } + ExprKind::Constructor(path, exprs, spread) => { + vis.visit_path_expr(&path); + walk_list!(vis, visit_field_expr, exprs); + if let Some(s) = spread { + vis.visit_path_expr(&s.path); + } + } } } diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index ac013bc9c1..1f68b9b1c0 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -110,6 +110,10 @@ impl AdtSortDef { (0..self.fields()).map(|i| FieldProj::Adt { def_id: self.did(), field: i as u32 }) } + pub fn field_names(&self) -> &Vec { + &self.0.field_names + } + pub fn field_by_name(&self, args: &[Sort], name: Symbol) -> Option<(FieldProj, Sort)> { let idx = self.0.field_names.iter().position(|it| name == *it)?; let proj = FieldProj::Adt { def_id: self.did(), field: idx as u32 }; diff --git a/crates/flux-syntax/src/grammar.lalrpop b/crates/flux-syntax/src/grammar.lalrpop index 80f1dd0589..f80d69a058 100644 --- a/crates/flux-syntax/src/grammar.lalrpop +++ b/crates/flux-syntax/src/grammar.lalrpop @@ -481,28 +481,46 @@ RefineArg: surface::RefineArg = { } }; -pub Expr = Level1; - -Level1 = NonAssoc; // <=> -Level2 = LeftAssoc; // => -Level3 = LeftAssoc; // || -Level4 = LeftAssoc; // && -Level5 = NonAssoc; // ==, !=, >=, <= -Level6 = LeftAssoc; // >>, << -Level7 = LeftAssoc; // +, - -Level8 = LeftAssoc; // *, %, / -Level9 = { - => { +pub Expr = Level1<"true">; + +Level1 = NonAssoc>; // <=> +Level2 = LeftAssoc>; // => +Level3 = LeftAssoc>; // || +Level4 = LeftAssoc>; // && +Level5 = NonAssoc>; // ==, !=, >=, <= +Level6 = LeftAssoc>; // >>, << +Level7 = LeftAssoc>; // +, - +Level8 = LeftAssoc>; // *, %, / +Level9 = { + > => { surface::Expr { kind: surface::ExprKind::UnaryOp(op, Box::new(e)), node_id: cx.next_node_id(), span: cx.map_span(lo, hi), } }, - -} -Level10: surface::Expr = { - "if" "{" "}" => { + > +} +Level10: surface::Expr = { + "{" > "}" if AllowStruct == "true" => { + surface::Expr { + kind: surface::ExprKind::Constructor(name, args, None) , + node_id: cx.next_node_id(), + span: cx.map_span(lo, hi), + } + }, + "{" > ".." "}" if AllowStruct == "true" => { + surface::Expr { + kind: surface::ExprKind::Constructor(name, args, Some(surface::Spread { + path: spread, + span: cx.map_span(spread_lo, spread_hi), + node_id: cx.next_node_id() + })), + node_id: cx.next_node_id(), + span: cx.map_span(lo, hi), + } + }, + "if" > "{" > "}" => { surface::Expr { kind: surface::ExprKind::IfThenElse(Box::new([p, e1, e2])), node_id: cx.next_node_id(), @@ -523,7 +541,7 @@ Level10: surface::Expr = { span: cx.map_span(lo, hi), } }, - "(" > ")" => { + "(" >> ")" => { surface::Expr { kind: surface::ExprKind::App(f, args), node_id: cx.next_node_id(), @@ -543,18 +561,29 @@ Level10: surface::Expr = { span: cx.map_span(lo, hi), } }, - "(" ")" + "(" > ")" +} + +ConstructorArgs: surface::FieldExpr = { + ":" > => { + surface::FieldExpr { + ident: name, + expr: arg, + node_id: cx.next_node_id(), + span: cx.map_span(lo, hi) + } + } } ElseIf: surface::Expr = { - "else" "if" "{" "}" => { + "else" "if" > "{" > "}" => { surface::Expr { kind: surface::ExprKind::IfThenElse(Box::new([p, e1, e2])), node_id: cx.next_node_id(), span: cx.map_span(lo, hi), } }, - "else" "{" "}" + "else" "{" > "}" } ExprPath: surface::ExprPath = { @@ -736,5 +765,6 @@ extern { "else" => Token::Else, "::" => Token::PathSep, "_" => Token::Underscore, + ".." => Token::DotDot, } } diff --git a/crates/flux-syntax/src/lexer.rs b/crates/flux-syntax/src/lexer.rs index db237c0ce9..9e227a6c52 100644 --- a/crates/flux-syntax/src/lexer.rs +++ b/crates/flux-syntax/src/lexer.rs @@ -68,6 +68,7 @@ pub enum Token { As, Hrn, Hdl, + DotDot, } pub(crate) struct Cursor<'t> { diff --git a/crates/flux-syntax/src/surface.rs b/crates/flux-syntax/src/surface.rs index 8f7909558d..2e99d6d9a4 100644 --- a/crates/flux-syntax/src/surface.rs +++ b/crates/flux-syntax/src/surface.rs @@ -446,6 +446,21 @@ pub enum GenericArgKind { Constraint(Ident, Ty), } +#[derive(Debug)] +pub struct FieldExpr { + pub ident: Ident, + pub expr: Expr, + pub span: Span, + pub node_id: NodeId, +} + +#[derive(Debug)] +pub struct Spread { + pub path: ExprPath, + pub span: Span, + pub node_id: NodeId, +} + #[derive(Debug)] pub struct Expr { pub kind: ExprKind, @@ -463,6 +478,7 @@ pub enum ExprKind { App(Ident, Vec), Alias(AliasReft, Vec), IfThenElse(Box<[Expr; 3]>), + Constructor(ExprPath, Vec, Option), } /// A [`Path`] but for refinement expressions diff --git a/crates/flux-syntax/src/surface/visit.rs b/crates/flux-syntax/src/surface/visit.rs index 5b450154ce..d9892b0d29 100644 --- a/crates/flux-syntax/src/surface/visit.rs +++ b/crates/flux-syntax/src/surface/visit.rs @@ -2,10 +2,10 @@ use rustc_span::symbol::Ident; use super::{ AliasReft, ArrayLen, Async, BaseSort, BaseTy, BaseTyKind, Ensures, EnumDef, Expr, ExprKind, - ExprPath, ExprPathSegment, FnInput, FnOutput, FnRetTy, FnSig, GenericArg, GenericArgKind, - GenericParam, Generics, Impl, ImplAssocReft, Indices, Lit, Path, PathSegment, Qualifier, - RefineArg, RefineParam, Sort, SortPath, SpecFunc, StructDef, Trait, TraitAssocReft, TraitRef, - Ty, TyAlias, TyKind, VariantDef, VariantRet, WhereBoundPredicate, + ExprPath, ExprPathSegment, FieldExpr, FnInput, FnOutput, FnRetTy, FnSig, GenericArg, + GenericArgKind, GenericParam, Generics, Impl, ImplAssocReft, Indices, Lit, Path, PathSegment, + Qualifier, RefineArg, RefineParam, Sort, SortPath, SpecFunc, StructDef, Trait, TraitAssocReft, + TraitRef, Ty, TyAlias, TyKind, VariantDef, VariantRet, WhereBoundPredicate, }; #[macro_export] @@ -153,6 +153,10 @@ pub trait Visitor: Sized { walk_expr(self, expr); } + fn visit_field_expr(&mut self, expr: &FieldExpr) { + walk_field_expr(self, expr); + } + fn visit_alias_pred(&mut self, alias_pred: &AliasReft) { walk_alias_pred(self, alias_pred); } @@ -462,6 +466,11 @@ pub fn walk_alias_pred(vis: &mut V, alias: &AliasReft) { vis.visit_ident(alias.name); } +pub fn walk_field_expr(vis: &mut V, expr: &FieldExpr) { + vis.visit_ident(expr.ident); + walk_expr(vis, &expr.expr); +} + pub fn walk_expr(vis: &mut V, expr: &Expr) { match &expr.kind { ExprKind::Path(qpath) => vis.visit_path_expr(qpath), @@ -489,6 +498,13 @@ pub fn walk_expr(vis: &mut V, expr: &Expr) { ExprKind::IfThenElse(box exprs) => { walk_list!(vis, visit_expr, exprs); } + ExprKind::Constructor(path, exprs, spread) => { + vis.visit_path_expr(path); + walk_list!(vis, visit_field_expr, exprs); + if let Some(s) = spread { + vis.visit_path_expr(&s.path); + } + } } } From c20b92ae2fa54ced1e581a999b6c40c75e468197 Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Fri, 15 Nov 2024 14:09:22 -0800 Subject: [PATCH 02/15] Add some tests for constructors --- tests/tests/neg/constructors/test00.rs | 14 ++++++++++++++ tests/tests/neg/constructors/test01.rs | 14 ++++++++++++++ tests/tests/neg/constructors/test02.rs | 14 ++++++++++++++ tests/tests/neg/constructors/test03.rs | 14 ++++++++++++++ tests/tests/pos/constructors/test00.rs | 14 ++++++++++++++ tests/tests/pos/constructors/test01.rs | 14 ++++++++++++++ 6 files changed, 84 insertions(+) create mode 100644 tests/tests/neg/constructors/test00.rs create mode 100644 tests/tests/neg/constructors/test01.rs create mode 100644 tests/tests/neg/constructors/test02.rs create mode 100644 tests/tests/neg/constructors/test03.rs create mode 100644 tests/tests/pos/constructors/test00.rs create mode 100644 tests/tests/pos/constructors/test01.rs diff --git a/tests/tests/neg/constructors/test00.rs b/tests/tests/neg/constructors/test00.rs new file mode 100644 index 0000000000..3cfcf0063f --- /dev/null +++ b/tests/tests/neg/constructors/test00.rs @@ -0,0 +1,14 @@ +#[flux::refined_by(x: int, y: int)] +pub struct X { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +#[flux::sig(fn (x: X[@old_x]) -> X[Y { y: 2, x: 1 }])] //~ ERROR cannot find value `Y` in this scope +fn f(mut x: X) -> X { + x.x = 1; + x.y = 2; + x +} diff --git a/tests/tests/neg/constructors/test01.rs b/tests/tests/neg/constructors/test01.rs new file mode 100644 index 0000000000..c40f707754 --- /dev/null +++ b/tests/tests/neg/constructors/test01.rs @@ -0,0 +1,14 @@ +#[flux::refined_by(x: int, y: int)] +pub struct X { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +#[flux::sig(fn (x: X[@old_x]) -> X[X { y: true, x: 1 }])] //~ ERROR mismatched sorts +fn f1(mut x: X) -> X { + x.x = 1; + x.y = 2; + x +} diff --git a/tests/tests/neg/constructors/test02.rs b/tests/tests/neg/constructors/test02.rs new file mode 100644 index 0000000000..5dd7e4772a --- /dev/null +++ b/tests/tests/neg/constructors/test02.rs @@ -0,0 +1,14 @@ +#[flux::refined_by(x: int, y: int)] +pub struct X { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +#[flux::sig(fn (x: X[@old_x]) -> X[X { y: 2, x: 1, z: 3 }])] //~ ERROR invalid field referenced in constructor +fn f1(mut x: X) -> X { + x.x = 1; + x.y = 2; + x +} diff --git a/tests/tests/neg/constructors/test03.rs b/tests/tests/neg/constructors/test03.rs new file mode 100644 index 0000000000..121d46486e --- /dev/null +++ b/tests/tests/neg/constructors/test03.rs @@ -0,0 +1,14 @@ +#[flux::refined_by(x: int, y: int)] +pub struct X { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +#[flux::sig(fn (x: X[@old_x]) -> X[X { y: 1, x: 1 }])] +fn f1(mut x: X) -> X { + x.x = 1; + x.y = 2; + x //~ ERROR refinement type error [E0999] +} diff --git a/tests/tests/pos/constructors/test00.rs b/tests/tests/pos/constructors/test00.rs new file mode 100644 index 0000000000..8e4ad180dd --- /dev/null +++ b/tests/tests/pos/constructors/test00.rs @@ -0,0 +1,14 @@ +#[flux::refined_by(x: int, y: int)] +pub struct X { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +#[flux::sig(fn (x: X[@old_x]) -> X[X { y: 2, x: 1 }])] +fn f(mut x: X) -> X { + x.x = 1; + x.y = 2; + x +} diff --git a/tests/tests/pos/constructors/test01.rs b/tests/tests/pos/constructors/test01.rs new file mode 100644 index 0000000000..fe78a2b1b8 --- /dev/null +++ b/tests/tests/pos/constructors/test01.rs @@ -0,0 +1,14 @@ +#[flux::refined_by(x: int, y: int)] +pub enum E { + #[flux::variant(E[0, 1])] + Variant1, + #[flux::variant(E[1, 2])] + Variant2, + #[flux::variant(E[2, 3])] + Variant3, +} + +#[flux::sig(fn (e: E[@old_enum]) -> E[E { x: 1, y: 2 }])] +fn f(e: E) -> E { + E::Variant2 +} From 8b35e2cef2afa44227ed7c8bd1e5d201565c3c82 Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Fri, 15 Nov 2024 14:24:33 -0800 Subject: [PATCH 03/15] Fix complex inner constructor case and add some tests for it --- .../src/resolver/refinement_resolver.rs | 7 ++++- tests/tests/neg/constructors/test04.rs | 29 +++++++++++++++++++ tests/tests/pos/constructors/test02.rs | 29 +++++++++++++++++++ 3 files changed, 64 insertions(+), 1 deletion(-) create mode 100644 tests/tests/neg/constructors/test04.rs create mode 100644 tests/tests/pos/constructors/test02.rs diff --git a/crates/flux-desugar/src/resolver/refinement_resolver.rs b/crates/flux-desugar/src/resolver/refinement_resolver.rs index 3f01a3d33b..1c9ed1f80d 100644 --- a/crates/flux-desugar/src/resolver/refinement_resolver.rs +++ b/crates/flux-desugar/src/resolver/refinement_resolver.rs @@ -296,8 +296,13 @@ impl surface::visit::Visitor for ScopedVisitorWrapper { self.on_func(*func, expr.node_id); } surface::ExprKind::Dot(path, _) => self.on_path(path), - surface::ExprKind::Constructor(path, _, spread) => { + surface::ExprKind::Constructor(path, field_exprs, spread) => { self.on_path(path); + // also need to deal with exprs in the constructor + // This is the case becasuse field exprs are different fields + for expr in field_exprs { + self.visit_expr(&expr.expr); + } if let Some(s) = spread { self.on_path(&s.path); } diff --git a/tests/tests/neg/constructors/test04.rs b/tests/tests/neg/constructors/test04.rs new file mode 100644 index 0000000000..d9a2e30ad3 --- /dev/null +++ b/tests/tests/neg/constructors/test04.rs @@ -0,0 +1,29 @@ +#![allow(unused)] + +#[flux::refined_by(x: int, y: int)] +pub struct X { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +#[flux::refined_by(x: X)] +pub struct Y { + #[flux::field(X[x])] + big_x: X, +} + +#[flux::sig(fn (x: X[@old_x]) -> X[X { y: 2, x: 1 }])] +fn f(mut x: X) -> X { + x.x = 1; + x.y = 2; + x +} + +#[flux::sig(fn (x: Y[@old_y]) -> Y[Y { x: X { x: 1, y: 1 } }])] +fn f_through_y(mut y: Y) -> Y { + y.big_x.x = 1; + y.big_x.y = 2; + y //~ ERROR refinement type error +} diff --git a/tests/tests/pos/constructors/test02.rs b/tests/tests/pos/constructors/test02.rs new file mode 100644 index 0000000000..f2d6d3bc9b --- /dev/null +++ b/tests/tests/pos/constructors/test02.rs @@ -0,0 +1,29 @@ +#![allow(unused)] + +#[flux::refined_by(x: int, y: int)] +pub struct X { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +#[flux::refined_by(x: X)] +pub struct Y { + #[flux::field(X[x])] + big_x: X, +} + +#[flux::sig(fn (x: X[@old_x]) -> X[X { y: 2, x: 1 }])] +fn f(mut x: X) -> X { + x.x = 1; + x.y = 2; + x +} + +#[flux::sig(fn (x: Y[@old_y]) -> Y[Y { x: X { x: 1, y: 2 } }])] +fn f_through_y(mut y: Y) -> Y { + y.big_x.x = 1; + y.big_x.y = 2; + y +} From 556c6395cb073acdc4d477f20b55e8716344d8ee Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Sat, 16 Nov 2024 09:37:00 -0800 Subject: [PATCH 04/15] Fix some issues and put tests in proper places --- .../src/resolver/refinement_resolver.rs | 7 +---- crates/flux-fhir-analysis/locales/en-US.ftl | 4 +++ crates/flux-fhir-analysis/src/conv/mod.rs | 26 +++++++---------- crates/flux-fhir-analysis/src/wf/errors.rs | 15 ++++++++++ .../flux-fhir-analysis/src/wf/param_usage.rs | 2 +- crates/flux-fhir-analysis/src/wf/sortck.rs | 13 +++------ crates/flux-syntax/src/surface/visit.rs | 2 +- tests/tests/neg/constructors/test00.rs | 6 ++-- tests/tests/neg/constructors/test01.rs | 19 ++++++++++-- tests/tests/neg/constructors/test04.rs | 29 ------------------- .../annot_check/constructor00.rs | 15 ++++++++++ .../annot_check/constructor01.rs} | 1 + .../wf/constructors00.rs} | 6 ++-- 13 files changed, 76 insertions(+), 69 deletions(-) delete mode 100644 tests/tests/neg/constructors/test04.rs create mode 100644 tests/tests/neg/error_messages/annot_check/constructor00.rs rename tests/tests/neg/{constructors/test02.rs => error_messages/annot_check/constructor01.rs} (90%) rename tests/tests/neg/{constructors/test03.rs => error_messages/wf/constructors00.rs} (55%) diff --git a/crates/flux-desugar/src/resolver/refinement_resolver.rs b/crates/flux-desugar/src/resolver/refinement_resolver.rs index 1c9ed1f80d..3f01a3d33b 100644 --- a/crates/flux-desugar/src/resolver/refinement_resolver.rs +++ b/crates/flux-desugar/src/resolver/refinement_resolver.rs @@ -296,13 +296,8 @@ impl surface::visit::Visitor for ScopedVisitorWrapper { self.on_func(*func, expr.node_id); } surface::ExprKind::Dot(path, _) => self.on_path(path), - surface::ExprKind::Constructor(path, field_exprs, spread) => { + surface::ExprKind::Constructor(path, _, spread) => { self.on_path(path); - // also need to deal with exprs in the constructor - // This is the case becasuse field exprs are different fields - for expr in field_exprs { - self.visit_expr(&expr.expr); - } if let Some(s) = spread { self.on_path(&s.path); } diff --git a/crates/flux-fhir-analysis/locales/en-US.ftl b/crates/flux-fhir-analysis/locales/en-US.ftl index ce8a2db2c3..8ea2ceb2e8 100644 --- a/crates/flux-fhir-analysis/locales/en-US.ftl +++ b/crates/flux-fhir-analysis/locales/en-US.ftl @@ -56,6 +56,10 @@ fhir_analysis_unexpected_fun = mismatched sorts .label = expected `{$sort}`, found function +fhir_analysis_unexpected_constructor = + mismatched sorts + .label = expected `{$sort}`, found constructor + fhir_analysis_param_count_mismatch = parameter count mismatch .label = this function has {$found -> diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 2fb969353a..e135db39b7 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -48,7 +48,7 @@ use rustc_target::spec::abi; use rustc_trait_selection::traits; use rustc_type_ir::DebruijnIndex; -use crate::{adt_sort_def_of, compare_impl_item::errors::InvalidAssocReft}; +use crate::compare_impl_item::errors::InvalidAssocReft; pub struct ConvCtxt<'genv, 'tcx, P> { genv: GlobalEnv<'genv, 'tcx>, @@ -1641,22 +1641,18 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, P> { exprs: &[fhir::FieldExpr], _spread: &Option, ) -> QueryResult> { - if let Some(local_def_id) = struct_def_id.as_local() { - let struct_adt = adt_sort_def_of(self.genv, local_def_id)?; - let field_names = struct_adt.field_names(); - let mut assns = Vec::new(); - for expr_val in exprs { - let field_symbol = expr_val.ident.name; - let pos = field_names.iter().position(|s| *s == field_symbol); - if let Some(idx) = pos { - assns.push((self.conv_expr(env, &expr_val.expr)?, idx)) - } + let struct_adt = self.genv.adt_sort_def_of(struct_def_id)?; + let field_names = struct_adt.field_names(); + let mut assns = Vec::new(); + for expr_val in exprs { + let field_symbol = expr_val.ident.name; + let pos = field_names.iter().position(|s| *s == field_symbol); + if let Some(idx) = pos { + assns.push((self.conv_expr(env, &expr_val.expr)?, idx)) } - assns.sort_by(|lhs, rhs| lhs.1.cmp(&rhs.1)); - Ok(assns.into_iter().map(|x| x.0).collect()) - } else { - todo!() } + assns.sort_by(|lhs, rhs| lhs.1.cmp(&rhs.1)); + Ok(assns.into_iter().map(|x| x.0).collect()) } fn conv_exprs(&mut self, env: &mut Env, exprs: &[fhir::Expr]) -> QueryResult> { diff --git a/crates/flux-fhir-analysis/src/wf/errors.rs b/crates/flux-fhir-analysis/src/wf/errors.rs index 532e08c459..bd6509958c 100644 --- a/crates/flux-fhir-analysis/src/wf/errors.rs +++ b/crates/flux-fhir-analysis/src/wf/errors.rs @@ -137,6 +137,21 @@ impl<'a> UnexpectedFun<'a> { } } +#[derive(Diagnostic)] +#[diag(fhir_analysis_unexpected_constructor, code = E0999)] +pub(super) struct UnexpectedConstructor<'a> { + #[primary_span] + #[label] + span: Span, + sort: &'a rty::Sort, +} + +impl<'a> UnexpectedConstructor<'a> { + pub(super) fn new(span: Span, sort: &'a rty::Sort) -> Self { + Self { span, sort } + } +} + #[derive(Diagnostic)] #[diag(fhir_analysis_invalid_field_update, code = E0999)] pub(super) struct InvalidFieldUpdate { diff --git a/crates/flux-fhir-analysis/src/wf/param_usage.rs b/crates/flux-fhir-analysis/src/wf/param_usage.rs index bd3fb513ba..e3248d5550 100644 --- a/crates/flux-fhir-analysis/src/wf/param_usage.rs +++ b/crates/flux-fhir-analysis/src/wf/param_usage.rs @@ -120,7 +120,7 @@ impl<'a, 'genv, 'tcx> ParamUsesChecker<'a, 'genv, 'tcx> { } fhir::ExprKind::Constructor(_path, exprs, _spread) => { for expr in exprs { - self.check_func_params_uses(&expr.expr, is_top_level_conj, is_top_level_var); + self.check_func_params_uses(&expr.expr, false, false); } } } diff --git a/crates/flux-fhir-analysis/src/wf/sortck.rs b/crates/flux-fhir-analysis/src/wf/sortck.rs index fa2a9b803d..130cf6c4c4 100644 --- a/crates/flux-fhir-analysis/src/wf/sortck.rs +++ b/crates/flux-fhir-analysis/src/wf/sortck.rs @@ -86,7 +86,7 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { fn check_constructor( &mut self, - path: &fhir::PathExpr, + expr_span: Span, field_exprs: &[fhir::FieldExpr], _spread: &Option, expected: &rty::Sort, @@ -108,12 +108,7 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { } Ok(()) } else { - Err(self.emit_err(errors::ArgCountMismatch::new( - Some(path.span), - String::from("type"), - 1, - field_exprs.len(), - ))) + Err(self.emit_err(errors::UnexpectedConstructor::new(expr_span, expected))) } } @@ -175,8 +170,8 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { self.check_abs(expr, refine_params, body, expected)? } fhir::ExprKind::Record(fields) => self.check_record(expr, fields, expected)?, - fhir::ExprKind::Constructor(path, exprs, spread) => { - self.check_constructor(path, exprs, spread, expected)? + fhir::ExprKind::Constructor(_path, exprs, spread) => { + self.check_constructor(expr.span, exprs, spread, expected)? } } Ok(()) diff --git a/crates/flux-syntax/src/surface/visit.rs b/crates/flux-syntax/src/surface/visit.rs index d9892b0d29..10c980c281 100644 --- a/crates/flux-syntax/src/surface/visit.rs +++ b/crates/flux-syntax/src/surface/visit.rs @@ -468,7 +468,7 @@ pub fn walk_alias_pred(vis: &mut V, alias: &AliasReft) { pub fn walk_field_expr(vis: &mut V, expr: &FieldExpr) { vis.visit_ident(expr.ident); - walk_expr(vis, &expr.expr); + vis.visit_expr(&expr.expr); } pub fn walk_expr(vis: &mut V, expr: &Expr) { diff --git a/tests/tests/neg/constructors/test00.rs b/tests/tests/neg/constructors/test00.rs index 3cfcf0063f..121d46486e 100644 --- a/tests/tests/neg/constructors/test00.rs +++ b/tests/tests/neg/constructors/test00.rs @@ -6,9 +6,9 @@ pub struct X { y: u32, } -#[flux::sig(fn (x: X[@old_x]) -> X[Y { y: 2, x: 1 }])] //~ ERROR cannot find value `Y` in this scope -fn f(mut x: X) -> X { +#[flux::sig(fn (x: X[@old_x]) -> X[X { y: 1, x: 1 }])] +fn f1(mut x: X) -> X { x.x = 1; x.y = 2; - x + x //~ ERROR refinement type error [E0999] } diff --git a/tests/tests/neg/constructors/test01.rs b/tests/tests/neg/constructors/test01.rs index c40f707754..d9a2e30ad3 100644 --- a/tests/tests/neg/constructors/test01.rs +++ b/tests/tests/neg/constructors/test01.rs @@ -1,3 +1,5 @@ +#![allow(unused)] + #[flux::refined_by(x: int, y: int)] pub struct X { #[flux::field(u32[x])] @@ -6,9 +8,22 @@ pub struct X { y: u32, } -#[flux::sig(fn (x: X[@old_x]) -> X[X { y: true, x: 1 }])] //~ ERROR mismatched sorts -fn f1(mut x: X) -> X { +#[flux::refined_by(x: X)] +pub struct Y { + #[flux::field(X[x])] + big_x: X, +} + +#[flux::sig(fn (x: X[@old_x]) -> X[X { y: 2, x: 1 }])] +fn f(mut x: X) -> X { x.x = 1; x.y = 2; x } + +#[flux::sig(fn (x: Y[@old_y]) -> Y[Y { x: X { x: 1, y: 1 } }])] +fn f_through_y(mut y: Y) -> Y { + y.big_x.x = 1; + y.big_x.y = 2; + y //~ ERROR refinement type error +} diff --git a/tests/tests/neg/constructors/test04.rs b/tests/tests/neg/constructors/test04.rs deleted file mode 100644 index d9a2e30ad3..0000000000 --- a/tests/tests/neg/constructors/test04.rs +++ /dev/null @@ -1,29 +0,0 @@ -#![allow(unused)] - -#[flux::refined_by(x: int, y: int)] -pub struct X { - #[flux::field(u32[x])] - x: u32, - #[flux::field(u32[y])] - y: u32, -} - -#[flux::refined_by(x: X)] -pub struct Y { - #[flux::field(X[x])] - big_x: X, -} - -#[flux::sig(fn (x: X[@old_x]) -> X[X { y: 2, x: 1 }])] -fn f(mut x: X) -> X { - x.x = 1; - x.y = 2; - x -} - -#[flux::sig(fn (x: Y[@old_y]) -> Y[Y { x: X { x: 1, y: 1 } }])] -fn f_through_y(mut y: Y) -> Y { - y.big_x.x = 1; - y.big_x.y = 2; - y //~ ERROR refinement type error -} diff --git a/tests/tests/neg/error_messages/annot_check/constructor00.rs b/tests/tests/neg/error_messages/annot_check/constructor00.rs new file mode 100644 index 0000000000..cc69492366 --- /dev/null +++ b/tests/tests/neg/error_messages/annot_check/constructor00.rs @@ -0,0 +1,15 @@ +#[flux::refined_by(x: int, y: int)] +pub struct X { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +// mismatched type inside of constructor (y should be int) +#[flux::sig(fn (x: X[@old_x]) -> X[X { y: true, x: 1 }])] //~ ERROR mismatched sorts +fn f1(mut x: X) -> X { + x.x = 1; + x.y = 2; + x +} diff --git a/tests/tests/neg/constructors/test02.rs b/tests/tests/neg/error_messages/annot_check/constructor01.rs similarity index 90% rename from tests/tests/neg/constructors/test02.rs rename to tests/tests/neg/error_messages/annot_check/constructor01.rs index 5dd7e4772a..4ff06740a3 100644 --- a/tests/tests/neg/constructors/test02.rs +++ b/tests/tests/neg/error_messages/annot_check/constructor01.rs @@ -6,6 +6,7 @@ pub struct X { y: u32, } +// z is not a valid field for X #[flux::sig(fn (x: X[@old_x]) -> X[X { y: 2, x: 1, z: 3 }])] //~ ERROR invalid field referenced in constructor fn f1(mut x: X) -> X { x.x = 1; diff --git a/tests/tests/neg/constructors/test03.rs b/tests/tests/neg/error_messages/wf/constructors00.rs similarity index 55% rename from tests/tests/neg/constructors/test03.rs rename to tests/tests/neg/error_messages/wf/constructors00.rs index 121d46486e..3cfcf0063f 100644 --- a/tests/tests/neg/constructors/test03.rs +++ b/tests/tests/neg/error_messages/wf/constructors00.rs @@ -6,9 +6,9 @@ pub struct X { y: u32, } -#[flux::sig(fn (x: X[@old_x]) -> X[X { y: 1, x: 1 }])] -fn f1(mut x: X) -> X { +#[flux::sig(fn (x: X[@old_x]) -> X[Y { y: 2, x: 1 }])] //~ ERROR cannot find value `Y` in this scope +fn f(mut x: X) -> X { x.x = 1; x.y = 2; - x //~ ERROR refinement type error [E0999] + x } From 35e859cc4685d13e0759776c63dbb4679464473f Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Mon, 18 Nov 2024 10:12:19 -0800 Subject: [PATCH 05/15] Move tests to proper directory --- tests/tests/neg/error_messages/wf/constructor00.rs | 14 ++++++++++++++ .../{annot_check => wf}/constructor01.rs | 0 .../constructor00.rs => wf/constructor02.rs} | 0 3 files changed, 14 insertions(+) create mode 100644 tests/tests/neg/error_messages/wf/constructor00.rs rename tests/tests/neg/error_messages/{annot_check => wf}/constructor01.rs (100%) rename tests/tests/neg/error_messages/{annot_check/constructor00.rs => wf/constructor02.rs} (100%) diff --git a/tests/tests/neg/error_messages/wf/constructor00.rs b/tests/tests/neg/error_messages/wf/constructor00.rs new file mode 100644 index 0000000000..3cfcf0063f --- /dev/null +++ b/tests/tests/neg/error_messages/wf/constructor00.rs @@ -0,0 +1,14 @@ +#[flux::refined_by(x: int, y: int)] +pub struct X { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +#[flux::sig(fn (x: X[@old_x]) -> X[Y { y: 2, x: 1 }])] //~ ERROR cannot find value `Y` in this scope +fn f(mut x: X) -> X { + x.x = 1; + x.y = 2; + x +} diff --git a/tests/tests/neg/error_messages/annot_check/constructor01.rs b/tests/tests/neg/error_messages/wf/constructor01.rs similarity index 100% rename from tests/tests/neg/error_messages/annot_check/constructor01.rs rename to tests/tests/neg/error_messages/wf/constructor01.rs diff --git a/tests/tests/neg/error_messages/annot_check/constructor00.rs b/tests/tests/neg/error_messages/wf/constructor02.rs similarity index 100% rename from tests/tests/neg/error_messages/annot_check/constructor00.rs rename to tests/tests/neg/error_messages/wf/constructor02.rs From 9b16d5b6bed55ae8eb8842575afb043d1bbb2f1b Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Mon, 18 Nov 2024 10:22:27 -0800 Subject: [PATCH 06/15] Improve invalid field error message --- crates/flux-fhir-analysis/src/wf/errors.rs | 14 -------------- crates/flux-fhir-analysis/src/wf/sortck.rs | 4 +++- tests/tests/neg/error_messages/wf/constructor01.rs | 2 +- 3 files changed, 4 insertions(+), 16 deletions(-) diff --git a/crates/flux-fhir-analysis/src/wf/errors.rs b/crates/flux-fhir-analysis/src/wf/errors.rs index bd6509958c..7084a9635c 100644 --- a/crates/flux-fhir-analysis/src/wf/errors.rs +++ b/crates/flux-fhir-analysis/src/wf/errors.rs @@ -152,20 +152,6 @@ impl<'a> UnexpectedConstructor<'a> { } } -#[derive(Diagnostic)] -#[diag(fhir_analysis_invalid_field_update, code = E0999)] -pub(super) struct InvalidFieldUpdate { - #[primary_span] - #[label] - span: Span, -} - -impl InvalidFieldUpdate { - pub(super) fn new(span: Span) -> Self { - Self { span } - } -} - #[derive(Diagnostic)] #[diag(fhir_analysis_param_count_mismatch, code = E0999)] pub(super) struct ParamCountMismatch { diff --git a/crates/flux-fhir-analysis/src/wf/sortck.rs b/crates/flux-fhir-analysis/src/wf/sortck.rs index 130cf6c4c4..0702b40027 100644 --- a/crates/flux-fhir-analysis/src/wf/sortck.rs +++ b/crates/flux-fhir-analysis/src/wf/sortck.rs @@ -103,7 +103,9 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { self.check_expr(&expr.expr, sort)? } else { // emit an error because we have a mismatched field - return Err(self.emit_err(errors::InvalidFieldUpdate::new(expr.ident.span))); + return Err( + self.emit_err(errors::FieldNotFound::new(expected.clone(), expr.ident)) + ); } } Ok(()) diff --git a/tests/tests/neg/error_messages/wf/constructor01.rs b/tests/tests/neg/error_messages/wf/constructor01.rs index 4ff06740a3..b6ef0c928a 100644 --- a/tests/tests/neg/error_messages/wf/constructor01.rs +++ b/tests/tests/neg/error_messages/wf/constructor01.rs @@ -7,7 +7,7 @@ pub struct X { } // z is not a valid field for X -#[flux::sig(fn (x: X[@old_x]) -> X[X { y: 2, x: 1, z: 3 }])] //~ ERROR invalid field referenced in constructor +#[flux::sig(fn (x: X[@old_x]) -> X[X { y: 2, x: 1, z: 3 }])] //~ ERROR no field `z` on sort `X` fn f1(mut x: X) -> X { x.x = 1; x.y = 2; From 18f6a6c37cfb47d7c25d5ba48ac016be533e6c58 Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Mon, 18 Nov 2024 10:46:12 -0800 Subject: [PATCH 07/15] Add missing fields error --- crates/flux-fhir-analysis/locales/en-US.ftl | 11 +++-- crates/flux-fhir-analysis/src/wf/errors.rs | 35 ++++++++++++++++ crates/flux-fhir-analysis/src/wf/sortck.rs | 45 ++++++++++++++++----- 3 files changed, 78 insertions(+), 13 deletions(-) diff --git a/crates/flux-fhir-analysis/locales/en-US.ftl b/crates/flux-fhir-analysis/locales/en-US.ftl index 8ea2ceb2e8..46b00fee5b 100644 --- a/crates/flux-fhir-analysis/locales/en-US.ftl +++ b/crates/flux-fhir-analysis/locales/en-US.ftl @@ -70,13 +70,16 @@ fhir_analysis_param_count_mismatch = *[other] {$expected} parameters } was expected -fhir_analysis_invalid_field_update = - invalid field referenced in constructor - .label = field does not exist - fhir_analysis_field_not_found = no field `{$fld}` on sort `{$sort}` +fhir_analysis_constructor_missing_fields = + missing fields in constructor: {$missing_fields} + +fhir_analysis_duplicate_field_used = + field `{$fld}` was previously used in constructor + .help = field `{$fld}` previously used here, consider removing it + fhir_analysis_invalid_primitive_dot_access = `{$sort}` is a primitive sort and therefore doesn't have fields diff --git a/crates/flux-fhir-analysis/src/wf/errors.rs b/crates/flux-fhir-analysis/src/wf/errors.rs index 7084a9635c..cb9a99b944 100644 --- a/crates/flux-fhir-analysis/src/wf/errors.rs +++ b/crates/flux-fhir-analysis/src/wf/errors.rs @@ -183,6 +183,41 @@ impl FieldNotFound { } } +#[derive(Diagnostic)] +#[diag(fhir_analysis_constructor_missing_fields, code = E0999)] +pub(super) struct ConstructorMissingFields { + #[primary_span] + constructor_span: Span, + missing_fields: String, +} + +impl ConstructorMissingFields { + pub(super) fn new(constructor_span: Span, missing_fields: Vec) -> Self { + let missing_fields = missing_fields + .into_iter() + .map(|x| format!("`{x}`")) + .collect::>() + .join(", "); + Self { constructor_span, missing_fields } + } +} + +#[derive(Diagnostic)] +#[diag(fhir_analysis_duplicate_field_used, code = E0999)] +pub(super) struct DuplicateFieldUsed { + #[primary_span] + span: Span, + fld: Ident, + #[help] + previous_span: Span, +} + +impl DuplicateFieldUsed { + pub(super) fn new(fld: Ident, previous_fld: Ident) -> Self { + Self { span: fld.span, fld, previous_span: previous_fld.span } + } +} + #[derive(Diagnostic)] #[diag(fhir_analysis_invalid_primitive_dot_access, code = E0999)] pub(super) struct InvalidPrimitiveDotAccess<'a> { diff --git a/crates/flux-fhir-analysis/src/wf/sortck.rs b/crates/flux-fhir-analysis/src/wf/sortck.rs index 0702b40027..9cdb2aa02e 100644 --- a/crates/flux-fhir-analysis/src/wf/sortck.rs +++ b/crates/flux-fhir-analysis/src/wf/sortck.rs @@ -88,27 +88,54 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { &mut self, expr_span: Span, field_exprs: &[fhir::FieldExpr], - _spread: &Option, + spread: &Option, expected: &rty::Sort, ) -> Result { if let rty::Sort::App(rty::SortCtor::Adt(sort_def), sort_args) = expected { // these are ordered - let field_names = sort_def.field_names(); - let sorts = sort_def.field_sorts(sort_args); + let mut fields_remaining = sort_def.field_names().clone(); + let mut sorts = sort_def.field_sorts(sort_args).to_vec(); + // keep a list of used fields + let mut fields_used = Vec::with_capacity(fields_remaining.capacity()); for expr in field_exprs { // make sure that the field is actually a field - if let Some(idx) = field_names.iter().position(|s| *s == expr.ident.name) { + if let Some(idx) = fields_remaining.iter().position(|s| *s == expr.ident.name) { // check that field sort is the same as the expr sort let sort = &sorts[idx]; - self.check_expr(&expr.expr, sort)? + let res = self.check_expr(&expr.expr, sort)?; + // remove the field from spread + fields_remaining.remove(idx); + // remove the field from sorts so it is identical to fields_remaining + sorts.remove(idx); + // push the field onto used fields + fields_used.push(expr.ident); + res } else { // emit an error because we have a mismatched field - return Err( - self.emit_err(errors::FieldNotFound::new(expected.clone(), expr.ident)) - ); + if let Some(idx) = fields_used.iter().position(|f| *f == expr.ident) { + // duplicate field error + return Err(self.emit_err(errors::DuplicateFieldUsed::new( + expr.ident, + fields_used[idx], + ))); + } else { + // non existent field found + return Err( + self.emit_err(errors::FieldNotFound::new(expected.clone(), expr.ident)) + ); + } } } - Ok(()) + if let Some(_spread) = spread { + // must check that the spread is of the same sort as the constructor + todo!() + } else if fields_remaining.len() > 0 { + // emit an error because all fields are not used + return Err(self + .emit_err(errors::ConstructorMissingFields::new(expr_span, fields_remaining))); + } else { + Ok(()) + } } else { Err(self.emit_err(errors::UnexpectedConstructor::new(expr_span, expected))) } From da86757965380f7454afa3f83bd1a78b4a59197c Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Mon, 18 Nov 2024 11:54:58 -0800 Subject: [PATCH 08/15] Add tests for new errors --- tests/tests/neg/error_messages/wf/constructor03.rs | 14 ++++++++++++++ .../wf/{constructors00.rs => constructor04.rs} | 2 +- 2 files changed, 15 insertions(+), 1 deletion(-) create mode 100644 tests/tests/neg/error_messages/wf/constructor03.rs rename tests/tests/neg/error_messages/wf/{constructors00.rs => constructor04.rs} (65%) diff --git a/tests/tests/neg/error_messages/wf/constructor03.rs b/tests/tests/neg/error_messages/wf/constructor03.rs new file mode 100644 index 0000000000..e485eda5fd --- /dev/null +++ b/tests/tests/neg/error_messages/wf/constructor03.rs @@ -0,0 +1,14 @@ +#[flux::refined_by(x: int, y: int)] +pub struct X { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +#[flux::sig(fn (x: X[@old_x]) -> X[X { y: 2, x: 1, x: 1 }])] //~ ERROR field `x` was previously used in constructor +fn f(mut x: X) -> X { + x.x = 1; + x.y = 2; + x +} diff --git a/tests/tests/neg/error_messages/wf/constructors00.rs b/tests/tests/neg/error_messages/wf/constructor04.rs similarity index 65% rename from tests/tests/neg/error_messages/wf/constructors00.rs rename to tests/tests/neg/error_messages/wf/constructor04.rs index 3cfcf0063f..07192576da 100644 --- a/tests/tests/neg/error_messages/wf/constructors00.rs +++ b/tests/tests/neg/error_messages/wf/constructor04.rs @@ -6,7 +6,7 @@ pub struct X { y: u32, } -#[flux::sig(fn (x: X[@old_x]) -> X[Y { y: 2, x: 1 }])] //~ ERROR cannot find value `Y` in this scope +#[flux::sig(fn (x: X[@old_x]) -> X[X { y: 2 }])] //~ ERROR missing fields in constructor: `x` fn f(mut x: X) -> X { x.x = 1; x.y = 2; From 42b0eda8b52f86dcd65062f79d56712435cefc79 Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Tue, 19 Nov 2024 07:54:43 -0800 Subject: [PATCH 09/15] cleanup sort checking --- crates/flux-fhir-analysis/src/wf/sortck.rs | 54 +++++++++------------- crates/flux-middle/src/rty/mod.rs | 14 +++++- 2 files changed, 35 insertions(+), 33 deletions(-) diff --git a/crates/flux-fhir-analysis/src/wf/sortck.rs b/crates/flux-fhir-analysis/src/wf/sortck.rs index 9cdb2aa02e..24b361b8ac 100644 --- a/crates/flux-fhir-analysis/src/wf/sortck.rs +++ b/crates/flux-fhir-analysis/src/wf/sortck.rs @@ -1,4 +1,4 @@ -use std::iter; +use std::{collections::HashSet, iter}; use ena::unify::InPlaceUnificationTable; use flux_common::{bug, iter::IterExt, result::ResultExt, span_bug, tracked_span_bug}; @@ -91,46 +91,36 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { spread: &Option, expected: &rty::Sort, ) -> Result { - if let rty::Sort::App(rty::SortCtor::Adt(sort_def), sort_args) = expected { - // these are ordered - let mut fields_remaining = sort_def.field_names().clone(); - let mut sorts = sort_def.field_sorts(sort_args).to_vec(); - // keep a list of used fields - let mut fields_used = Vec::with_capacity(fields_remaining.capacity()); + if let rty::Sort::App(rty::SortCtor::Adt(sort_def), _) = expected { + let sort_by_field_name = sort_def.sort_by_field_name(); + let mut used_fields = HashSet::new(); + for expr in field_exprs { // make sure that the field is actually a field - if let Some(idx) = fields_remaining.iter().position(|s| *s == expr.ident.name) { - // check that field sort is the same as the expr sort - let sort = &sorts[idx]; - let res = self.check_expr(&expr.expr, sort)?; - // remove the field from spread - fields_remaining.remove(idx); - // remove the field from sorts so it is identical to fields_remaining - sorts.remove(idx); - // push the field onto used fields - fields_used.push(expr.ident); - res + if let Some(sort) = sort_by_field_name.get(&expr.ident.name) { + self.check_expr(&expr.expr, sort)?; } else { - // emit an error because we have a mismatched field - if let Some(idx) = fields_used.iter().position(|f| *f == expr.ident) { - // duplicate field error - return Err(self.emit_err(errors::DuplicateFieldUsed::new( - expr.ident, - fields_used[idx], - ))); - } else { - // non existent field found - return Err( - self.emit_err(errors::FieldNotFound::new(expected.clone(), expr.ident)) - ); - } + return Err( + self.emit_err(errors::FieldNotFound::new(expected.clone(), expr.ident)) + ); + } + if let Some(old_field) = used_fields.replace(expr.ident) { + return Err( + self.emit_err(errors::DuplicateFieldUsed::new(expr.ident, old_field)) + ); } } if let Some(_spread) = spread { // must check that the spread is of the same sort as the constructor todo!() - } else if fields_remaining.len() > 0 { + } else if sort_by_field_name.len() != used_fields.len() { // emit an error because all fields are not used + let used_field_names: Vec = + used_fields.into_iter().map(|k| k.name).collect(); + let fields_remaining = sort_by_field_name + .into_keys() + .filter(|x| !used_field_names.contains(x)) + .collect(); return Err(self .emit_err(errors::ConstructorMissingFields::new(expr_span, fields_remaining))); } else { diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 1f68b9b1c0..31a1ed9e0f 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -14,7 +14,7 @@ mod pretty; pub mod projections; pub mod refining; pub mod subst; -use std::{borrow::Cow, cmp::Ordering, hash::Hash, iter, sync::LazyLock}; +use std::{borrow::Cow, cmp::Ordering, collections::HashMap, hash::Hash, iter, sync::LazyLock}; pub use binder::{Binder, BoundReftKind, BoundVariableKind, BoundVariableKinds, EarlyBinder}; pub use evars::{EVar, EVarGen}; @@ -114,6 +114,18 @@ impl AdtSortDef { &self.0.field_names } + pub fn sort_by_field_name(&self) -> HashMap { + let mut map = HashMap::new(); + self.0 + .sorts + .iter() + .zip(self.0.field_names.iter()) + .for_each(|(sort, field_name)| { + map.insert(*field_name, sort); + }); + map + } + pub fn field_by_name(&self, args: &[Sort], name: Symbol) -> Option<(FieldProj, Sort)> { let idx = self.0.field_names.iter().position(|it| name == *it)?; let proj = FieldProj::Adt { def_id: self.did(), field: idx as u32 }; From 3cfee1fcc8275427c58ed9491f4a234f07a12294 Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Tue, 19 Nov 2024 09:34:51 -0800 Subject: [PATCH 10/15] Add support for spreads --- crates/flux-desugar/locales/en-US.ftl | 7 ++ crates/flux-desugar/src/desugar.rs | 82 ++++++++++++++----- crates/flux-desugar/src/errors.rs | 22 +++++ .../src/resolver/refinement_resolver.rs | 17 ++-- crates/flux-fhir-analysis/src/conv/mod.rs | 40 ++++++++- crates/flux-fhir-analysis/src/wf/sortck.rs | 24 ++++-- crates/flux-middle/src/rty/mod.rs | 18 +++- crates/flux-syntax/src/grammar.lalrpop | 26 +++--- crates/flux-syntax/src/lexer.rs | 1 + crates/flux-syntax/src/surface.rs | 8 +- crates/flux-syntax/src/surface/visit.rs | 24 +++--- .../error_messages/desugar/constructor00.rs | 16 ++++ .../neg/error_messages/wf/constructor05.rs | 26 ++++++ tests/tests/pos/constructors/test03.rs | 14 ++++ 14 files changed, 259 insertions(+), 66 deletions(-) create mode 100644 tests/tests/neg/error_messages/desugar/constructor00.rs create mode 100644 tests/tests/neg/error_messages/wf/constructor05.rs create mode 100644 tests/tests/pos/constructors/test03.rs diff --git a/crates/flux-desugar/locales/en-US.ftl b/crates/flux-desugar/locales/en-US.ftl index a3b66f2beb..ba5c16b826 100644 --- a/crates/flux-desugar/locales/en-US.ftl +++ b/crates/flux-desugar/locales/en-US.ftl @@ -16,6 +16,9 @@ desugar_invalid_dot_var = desugar_invalid_constructor_path = invalid use of path in constructor +desugar_invalid_constructor_spread = + invalid spread in constructor + desugar_invalid_func_as_var = invalid use of function .label = function not supported in this position @@ -38,6 +41,10 @@ desugar_unresolved_generic_param = desugar_invalid_variant_ret = invalid variant return type +desugar_multiple_spreads_in_constructor = + multiple spreads found in constructor + .help = previous spread found here. consider removing it + # Resolve errors desugar_duplicate_param = diff --git a/crates/flux-desugar/src/desugar.rs b/crates/flux-desugar/src/desugar.rs index aa9dd5f828..819a81619b 100644 --- a/crates/flux-desugar/src/desugar.rs +++ b/crates/flux-desugar/src/desugar.rs @@ -9,7 +9,7 @@ use flux_middle::{ try_alloc_slice, MaybeExternId, ResolverOutput, }; use flux_syntax::{ - surface::{self, visit::Visitor as _, NodeId}, + surface::{self, visit::Visitor as _, ConstructorArgs, FieldExpr, NodeId, Spread}, walk_list, }; use hir::{def::DefKind, ItemKind}; @@ -1389,35 +1389,73 @@ trait DesugarCtxt<'genv, 'tcx: 'genv> { self.genv().alloc(e2?), ) } - surface::ExprKind::Constructor(path, constructor_args, spread) => { + surface::ExprKind::Constructor(path, constructor_args) => { let path = self.desugar_constructor_path(path)?; - let constructor_args = - try_alloc_slice!(self.genv(), constructor_args, |field_expr| { - let e = self.desugar_expr(&field_expr.expr)?; - Ok(fhir::FieldExpr { - ident: field_expr.ident, - expr: e, - fhir_id: self.next_fhir_id(), - span: e.span, - }) - })?; - let spread = match spread { - None => None, - Some(s) => { - Some(fhir::Spread { - path: self.desugar_constructor_path(&s.path)?, - span: s.span, - fhir_id: self.next_fhir_id(), - }) - } + let field_exprs = constructor_args + .iter() + .filter_map(|arg| { + match arg { + ConstructorArgs::FieldExpr(e) => Some(e), + ConstructorArgs::Spread(_) => None, + } + }) + .collect::>(); + + let field_exprs = try_alloc_slice!(self.genv(), field_exprs, |field_expr| { + let e = self.desugar_expr(&field_expr.expr)?; + Ok(fhir::FieldExpr { + ident: field_expr.ident, + expr: e, + fhir_id: self.next_fhir_id(), + span: e.span, + }) + })?; + + let spreads = constructor_args + .iter() + .filter_map(|arg| { + match arg { + ConstructorArgs::FieldExpr(_) => None, + ConstructorArgs::Spread(s) => Some(s), + } + }) + .collect::>(); + + let spread = if spreads.len() == 0 { + None + } else if spreads.len() == 1 { + let s = spreads[0]; + Some(fhir::Spread { + path: self.desugar_spread_path(&s.path)?, + span: s.span, + fhir_id: self.next_fhir_id(), + }) + } else { + // Multiple spreads found - emit and error + return Err(self.emit_err(errors::MultipleSpreadsInConstructor::new( + &spreads[1].path, + &spreads[0].path, + ))); }; - fhir::ExprKind::Constructor(path, constructor_args, spread) + fhir::ExprKind::Constructor(path, field_exprs, spread) } }; Ok(fhir::Expr { kind, span: expr.span, fhir_id: self.next_fhir_id() }) } + fn desugar_spread_path(&self, path: &surface::ExprPath) -> Result> { + let res = self.resolver_output().expr_path_res_map[&path.node_id]; + if let ExprRes::Param(..) = res { + let segments = self + .genv() + .alloc_slice_fill_iter(path.segments.iter().map(|s| s.ident)); + Ok(fhir::PathExpr { segments, res, fhir_id: self.next_fhir_id(), span: path.span }) + } else { + Err(self.emit_err(errors::InvalidConstructorSpread { span: path.span })) + } + } + fn desugar_constructor_path(&self, path: &surface::ExprPath) -> Result> { let res = self.resolver_output().expr_path_res_map[&path.node_id]; if let ExprRes::Struct(..) | ExprRes::Enum(..) = res { diff --git a/crates/flux-desugar/src/errors.rs b/crates/flux-desugar/src/errors.rs index f8e9158d11..340e3e6a5e 100644 --- a/crates/flux-desugar/src/errors.rs +++ b/crates/flux-desugar/src/errors.rs @@ -24,6 +24,13 @@ pub(super) struct InvalidConstructorPath { pub(super) span: Span, } +#[derive(Diagnostic)] +#[diag(desugar_invalid_constructor_spread, code = E0999)] +pub(super) struct InvalidConstructorSpread { + #[primary_span] + pub(super) span: Span, +} + #[derive(Diagnostic)] #[diag(desugar_invalid_dot_var, code = E0999)] pub(super) struct InvalidDotVar { @@ -109,3 +116,18 @@ impl InvalidVariantRet { Self { span: path.span } } } + +#[derive(Diagnostic)] +#[diag(desugar_multiple_spreads_in_constructor, code = E0999)] +pub(super) struct MultipleSpreadsInConstructor { + #[primary_span] + pub(super) span: Span, + #[help] + pub(super) prev_span: Span, +} + +impl MultipleSpreadsInConstructor { + pub(super) fn new(path: &surface::ExprPath, prev_path: &surface::ExprPath) -> Self { + Self { span: path.span, prev_span: prev_path.span } + } +} diff --git a/crates/flux-desugar/src/resolver/refinement_resolver.rs b/crates/flux-desugar/src/resolver/refinement_resolver.rs index 3f01a3d33b..f037b7685a 100644 --- a/crates/flux-desugar/src/resolver/refinement_resolver.rs +++ b/crates/flux-desugar/src/resolver/refinement_resolver.rs @@ -7,7 +7,7 @@ use flux_middle::{ ResolverOutput, }; use flux_syntax::{ - surface::{self, visit::Visitor as _, Ident, NodeId}, + surface::{self, visit::Visitor as _, ConstructorArgs, Ident, NodeId}, walk_list, }; use rustc_data_structures::{ @@ -296,11 +296,18 @@ impl surface::visit::Visitor for ScopedVisitorWrapper { self.on_func(*func, expr.node_id); } surface::ExprKind::Dot(path, _) => self.on_path(path), - surface::ExprKind::Constructor(path, _, spread) => { + surface::ExprKind::Constructor(path, args) => { + // walk constructor path self.on_path(path); - if let Some(s) = spread { - self.on_path(&s.path); - } + // walk spread if there is one + args.iter() + .filter_map(|arg| { + match arg { + ConstructorArgs::FieldExpr(_) => None, + ConstructorArgs::Spread(s) => Some(s), + } + }) + .for_each(|arg| self.on_path(&arg.path)); } _ => {} } diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index e135db39b7..4640195fb9 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -1639,17 +1639,49 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, P> { struct_def_id: DefId, env: &mut Env, exprs: &[fhir::FieldExpr], - _spread: &Option, + spread: &Option, ) -> QueryResult> { let struct_adt = self.genv.adt_sort_def_of(struct_def_id)?; - let field_names = struct_adt.field_names(); + let sort_and_idx_by_field = struct_adt.sort_and_idx_by_field_name(); + let mut used_fields = FxHashSet::default(); let mut assns = Vec::new(); for expr_val in exprs { let field_symbol = expr_val.ident.name; - let pos = field_names.iter().position(|s| *s == field_symbol); - if let Some(idx) = pos { + if let Some((idx, _)) = sort_and_idx_by_field.get(&field_symbol) { assns.push((self.conv_expr(env, &expr_val.expr)?, idx)) } + used_fields.replace(field_symbol); + } + if let Some(spread) = spread { + // compute the unused fields and + // create projections from unused fields + // and push them into assignments + sort_and_idx_by_field + .iter() + .filter_map(|(fld, (idx, _))| { + match used_fields.get(fld) { + None => { + match spread.path.res { + ExprRes::Param(..) => { + let expr = env.lookup(&spread.path).to_expr(); + let proj = rty::FieldProj::Adt { + def_id: struct_def_id, + field: *idx as u32, + }; + Some((rty::Expr::field_proj(expr, proj), idx)) + } + _ => { + span_bug!( + spread.span, + "unexpected path in constructor's spread after desugaring" + ) + } + } + } + Some(_) => None, + } + }) + .for_each(|proj| assns.push(proj)); } assns.sort_by(|lhs, rhs| lhs.1.cmp(&rhs.1)); Ok(assns.into_iter().map(|x| x.0).collect()) diff --git a/crates/flux-fhir-analysis/src/wf/sortck.rs b/crates/flux-fhir-analysis/src/wf/sortck.rs index 24b361b8ac..0cb2c08f35 100644 --- a/crates/flux-fhir-analysis/src/wf/sortck.rs +++ b/crates/flux-fhir-analysis/src/wf/sortck.rs @@ -1,4 +1,4 @@ -use std::{collections::HashSet, iter}; +use std::iter; use ena::unify::InPlaceUnificationTable; use flux_common::{bug, iter::IterExt, result::ResultExt, span_bug, tracked_span_bug}; @@ -16,7 +16,7 @@ use flux_middle::{ use itertools::{izip, Itertools}; use rustc_data_structures::unord::UnordMap; use rustc_errors::Diagnostic; -use rustc_hash::FxHashMap; +use rustc_hash::{FxHashMap, FxHashSet}; use rustc_span::{def_id::DefId, symbol::Ident, Span}; use super::errors; @@ -93,7 +93,7 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { ) -> Result { if let rty::Sort::App(rty::SortCtor::Adt(sort_def), _) = expected { let sort_by_field_name = sort_def.sort_by_field_name(); - let mut used_fields = HashSet::new(); + let mut used_fields = FxHashSet::default(); for expr in field_exprs { // make sure that the field is actually a field @@ -110,9 +110,23 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { ); } } - if let Some(_spread) = spread { + if let Some(spread) = spread { // must check that the spread is of the same sort as the constructor - todo!() + match spread.path.res { + ExprRes::Param(_, id) => { + let found = self.param_sort(id); + if !self.is_coercible(&found, expected, spread.fhir_id) { + return Err(self.emit_sort_mismatch(spread.span, &expected, &found)); + } + } + _ => { + span_bug!( + spread.span, + "unexpected path in constructor's spread after desugaring" + ) + } + } + Ok(()) } else if sort_by_field_name.len() != used_fields.len() { // emit an error because all fields are not used let used_field_names: Vec = diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 31a1ed9e0f..8219f1b712 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -40,6 +40,7 @@ use flux_rustc_bridge::{ use itertools::Itertools; pub use normalize::SpecFuncDefns; use rustc_data_structures::unord::UnordMap; +use rustc_hash::FxHashMap; use rustc_hir::{def_id::DefId, LangItem, Safety}; use rustc_index::{newtype_index, IndexSlice}; use rustc_macros::{extension, Decodable, Encodable, TyDecodable, TyEncodable}; @@ -114,8 +115,8 @@ impl AdtSortDef { &self.0.field_names } - pub fn sort_by_field_name(&self) -> HashMap { - let mut map = HashMap::new(); + pub fn sort_by_field_name(&self) -> FxHashMap { + let mut map = FxHashMap::default(); self.0 .sorts .iter() @@ -126,6 +127,19 @@ impl AdtSortDef { map } + pub fn sort_and_idx_by_field_name(&self) -> HashMap { + let mut map = HashMap::new(); + self.0 + .sorts + .iter() + .zip(self.0.field_names.iter()) + .enumerate() + .for_each(|(idx, (sort, field_name))| { + map.insert(*field_name, (idx, sort)); + }); + map + } + pub fn field_by_name(&self, args: &[Sort], name: Symbol) -> Option<(FieldProj, Sort)> { let idx = self.0.field_names.iter().position(|it| name == *it)?; let proj = FieldProj::Adt { def_id: self.did(), field: idx as u32 }; diff --git a/crates/flux-syntax/src/grammar.lalrpop b/crates/flux-syntax/src/grammar.lalrpop index f80d69a058..46578f370b 100644 --- a/crates/flux-syntax/src/grammar.lalrpop +++ b/crates/flux-syntax/src/grammar.lalrpop @@ -504,18 +504,7 @@ Level9 = { Level10: surface::Expr = { "{" > "}" if AllowStruct == "true" => { surface::Expr { - kind: surface::ExprKind::Constructor(name, args, None) , - node_id: cx.next_node_id(), - span: cx.map_span(lo, hi), - } - }, - "{" > ".." "}" if AllowStruct == "true" => { - surface::Expr { - kind: surface::ExprKind::Constructor(name, args, Some(surface::Spread { - path: spread, - span: cx.map_span(spread_lo, spread_hi), - node_id: cx.next_node_id() - })), + kind: surface::ExprKind::Constructor(name, args) , node_id: cx.next_node_id(), span: cx.map_span(lo, hi), } @@ -564,14 +553,21 @@ Level10: surface::Expr = { "(" > ")" } -ConstructorArgs: surface::FieldExpr = { +ConstructorArgs: surface::ConstructorArgs = { ":" > => { - surface::FieldExpr { + surface::ConstructorArgs::FieldExpr(surface::FieldExpr { ident: name, expr: arg, node_id: cx.next_node_id(), span: cx.map_span(lo, hi) - } + }) + }, + ".." => { + surface::ConstructorArgs::Spread(surface::Spread { + path: spread, + node_id: cx.next_node_id(), + span: cx.map_span(lo, hi) + }) } } diff --git a/crates/flux-syntax/src/lexer.rs b/crates/flux-syntax/src/lexer.rs index 9e227a6c52..770fd650d3 100644 --- a/crates/flux-syntax/src/lexer.rs +++ b/crates/flux-syntax/src/lexer.rs @@ -189,6 +189,7 @@ impl<'t> Cursor<'t> { } TokenKind::Not => Token::Not, TokenKind::PathSep => Token::PathSep, + TokenKind::DotDot => Token::DotDot, _ => Token::Invalid, }; self.push_token(span.lo(), token, span.hi()); diff --git a/crates/flux-syntax/src/surface.rs b/crates/flux-syntax/src/surface.rs index 2e99d6d9a4..a2745cdba9 100644 --- a/crates/flux-syntax/src/surface.rs +++ b/crates/flux-syntax/src/surface.rs @@ -461,6 +461,12 @@ pub struct Spread { pub node_id: NodeId, } +#[derive(Debug)] +pub enum ConstructorArgs { + FieldExpr(FieldExpr), + Spread(Spread), +} + #[derive(Debug)] pub struct Expr { pub kind: ExprKind, @@ -478,7 +484,7 @@ pub enum ExprKind { App(Ident, Vec), Alias(AliasReft, Vec), IfThenElse(Box<[Expr; 3]>), - Constructor(ExprPath, Vec, Option), + Constructor(ExprPath, Vec), } /// A [`Path`] but for refinement expressions diff --git a/crates/flux-syntax/src/surface/visit.rs b/crates/flux-syntax/src/surface/visit.rs index 10c980c281..a83f93e60c 100644 --- a/crates/flux-syntax/src/surface/visit.rs +++ b/crates/flux-syntax/src/surface/visit.rs @@ -1,11 +1,11 @@ use rustc_span::symbol::Ident; use super::{ - AliasReft, ArrayLen, Async, BaseSort, BaseTy, BaseTyKind, Ensures, EnumDef, Expr, ExprKind, - ExprPath, ExprPathSegment, FieldExpr, FnInput, FnOutput, FnRetTy, FnSig, GenericArg, - GenericArgKind, GenericParam, Generics, Impl, ImplAssocReft, Indices, Lit, Path, PathSegment, - Qualifier, RefineArg, RefineParam, Sort, SortPath, SpecFunc, StructDef, Trait, TraitAssocReft, - TraitRef, Ty, TyAlias, TyKind, VariantDef, VariantRet, WhereBoundPredicate, + AliasReft, ArrayLen, Async, BaseSort, BaseTy, BaseTyKind, ConstructorArgs, Ensures, EnumDef, + Expr, ExprKind, ExprPath, ExprPathSegment, FieldExpr, FnInput, FnOutput, FnRetTy, FnSig, + GenericArg, GenericArgKind, GenericParam, Generics, Impl, ImplAssocReft, Indices, Lit, Path, + PathSegment, Qualifier, RefineArg, RefineParam, Sort, SortPath, SpecFunc, StructDef, Trait, + TraitAssocReft, TraitRef, Ty, TyAlias, TyKind, VariantDef, VariantRet, WhereBoundPredicate, }; #[macro_export] @@ -153,8 +153,11 @@ pub trait Visitor: Sized { walk_expr(self, expr); } - fn visit_field_expr(&mut self, expr: &FieldExpr) { - walk_field_expr(self, expr); + fn visit_constructor_args(&mut self, expr: &ConstructorArgs) { + match expr { + ConstructorArgs::FieldExpr(field_expr) => walk_field_expr(self, field_expr), + ConstructorArgs::Spread(spread) => walk_path_expr(self, &spread.path), + } } fn visit_alias_pred(&mut self, alias_pred: &AliasReft) { @@ -498,12 +501,9 @@ pub fn walk_expr(vis: &mut V, expr: &Expr) { ExprKind::IfThenElse(box exprs) => { walk_list!(vis, visit_expr, exprs); } - ExprKind::Constructor(path, exprs, spread) => { + ExprKind::Constructor(path, exprs) => { vis.visit_path_expr(path); - walk_list!(vis, visit_field_expr, exprs); - if let Some(s) = spread { - vis.visit_path_expr(&s.path); - } + walk_list!(vis, visit_constructor_args, exprs); } } } diff --git a/tests/tests/neg/error_messages/desugar/constructor00.rs b/tests/tests/neg/error_messages/desugar/constructor00.rs new file mode 100644 index 0000000000..9df3a5331c --- /dev/null +++ b/tests/tests/neg/error_messages/desugar/constructor00.rs @@ -0,0 +1,16 @@ +#[flux::refined_by(x: int, y: int)] +pub struct S { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +impl S { + // multiple spreads in constructor + #[flux::sig(fn (self: &strg S[@old_x]) ensures self: S[S { x: 1, ..old_x, ..old_x }])] //~ERROR multiple spreads found in constructor + pub fn foo(&mut self) { + self.x = 1; + self.y = 1; + } +} diff --git a/tests/tests/neg/error_messages/wf/constructor05.rs b/tests/tests/neg/error_messages/wf/constructor05.rs new file mode 100644 index 0000000000..ad3ed908e2 --- /dev/null +++ b/tests/tests/neg/error_messages/wf/constructor05.rs @@ -0,0 +1,26 @@ +#[flux::refined_by(x: int, y: int)] +pub struct S { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +#[flux::refined_by(x: int, y: int)] +pub enum E { + #[flux::variant(E[0, 1])] + VariantOne, + #[flux::variant(E[1, 2])] + VariantTwo, + #[flux::variant(E[2, 3])] + VariantThree, +} + +impl S { + // The constructor's spread `..e` is wrong + #[flux::sig(fn (self: &strg S[@old_x], E[@e]) ensures self: S[S { x: 1, ..e }])] //~ERROR mismatched sorts + pub fn crazy(&mut self, _e: E) { + self.x = 1; + self.y = 1; + } +} diff --git a/tests/tests/pos/constructors/test03.rs b/tests/tests/pos/constructors/test03.rs new file mode 100644 index 0000000000..a15d1bb987 --- /dev/null +++ b/tests/tests/pos/constructors/test03.rs @@ -0,0 +1,14 @@ +#[flux::refined_by(x: int, y: int)] +pub struct S { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +impl S { + #[flux::sig(fn (self: &strg S[@old_x]) ensures self: S[S { x: 1, ..old_x }])] + pub fn update(&mut self) { + self.x = 1; + } +} From 0cb56b3785aaace8da20ed98e04dc25446bf0ff7 Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Tue, 19 Nov 2024 11:04:37 -0800 Subject: [PATCH 11/15] Spreads as aribitrary expressions --- crates/flux-desugar/locales/en-US.ftl | 3 -- crates/flux-desugar/src/desugar.rs | 23 ++++---------- crates/flux-desugar/src/errors.rs | 11 ++----- .../src/resolver/refinement_resolver.rs | 14 ++------- crates/flux-fhir-analysis/src/conv/mod.rs | 31 ++++++------------- crates/flux-fhir-analysis/src/wf/sortck.rs | 17 ++-------- crates/flux-middle/src/fhir.rs | 4 +-- crates/flux-middle/src/fhir/visit.rs | 2 +- crates/flux-middle/src/rty/mod.rs | 22 +++---------- crates/flux-syntax/src/grammar.lalrpop | 4 +-- crates/flux-syntax/src/surface.rs | 2 +- crates/flux-syntax/src/surface/visit.rs | 2 +- tests/tests/pos/constructors/test04.rs | 23 ++++++++++++++ 13 files changed, 56 insertions(+), 102 deletions(-) create mode 100644 tests/tests/pos/constructors/test04.rs diff --git a/crates/flux-desugar/locales/en-US.ftl b/crates/flux-desugar/locales/en-US.ftl index ba5c16b826..5c74c6f153 100644 --- a/crates/flux-desugar/locales/en-US.ftl +++ b/crates/flux-desugar/locales/en-US.ftl @@ -16,9 +16,6 @@ desugar_invalid_dot_var = desugar_invalid_constructor_path = invalid use of path in constructor -desugar_invalid_constructor_spread = - invalid spread in constructor - desugar_invalid_func_as_var = invalid use of function .label = function not supported in this position diff --git a/crates/flux-desugar/src/desugar.rs b/crates/flux-desugar/src/desugar.rs index 819a81619b..d3d87426bc 100644 --- a/crates/flux-desugar/src/desugar.rs +++ b/crates/flux-desugar/src/desugar.rs @@ -1425,16 +1425,17 @@ trait DesugarCtxt<'genv, 'tcx: 'genv> { None } else if spreads.len() == 1 { let s = spreads[0]; - Some(fhir::Spread { - path: self.desugar_spread_path(&s.path)?, + let spread = fhir::Spread { + expr: self.desugar_expr(&s.expr)?, span: s.span, fhir_id: self.next_fhir_id(), - }) + }; + Some(self.genv().alloc(spread)) } else { // Multiple spreads found - emit and error return Err(self.emit_err(errors::MultipleSpreadsInConstructor::new( - &spreads[1].path, - &spreads[0].path, + spreads[1].span, + spreads[0].span, ))); }; fhir::ExprKind::Constructor(path, field_exprs, spread) @@ -1444,18 +1445,6 @@ trait DesugarCtxt<'genv, 'tcx: 'genv> { Ok(fhir::Expr { kind, span: expr.span, fhir_id: self.next_fhir_id() }) } - fn desugar_spread_path(&self, path: &surface::ExprPath) -> Result> { - let res = self.resolver_output().expr_path_res_map[&path.node_id]; - if let ExprRes::Param(..) = res { - let segments = self - .genv() - .alloc_slice_fill_iter(path.segments.iter().map(|s| s.ident)); - Ok(fhir::PathExpr { segments, res, fhir_id: self.next_fhir_id(), span: path.span }) - } else { - Err(self.emit_err(errors::InvalidConstructorSpread { span: path.span })) - } - } - fn desugar_constructor_path(&self, path: &surface::ExprPath) -> Result> { let res = self.resolver_output().expr_path_res_map[&path.node_id]; if let ExprRes::Struct(..) | ExprRes::Enum(..) = res { diff --git a/crates/flux-desugar/src/errors.rs b/crates/flux-desugar/src/errors.rs index 340e3e6a5e..5dc2b4ed14 100644 --- a/crates/flux-desugar/src/errors.rs +++ b/crates/flux-desugar/src/errors.rs @@ -24,13 +24,6 @@ pub(super) struct InvalidConstructorPath { pub(super) span: Span, } -#[derive(Diagnostic)] -#[diag(desugar_invalid_constructor_spread, code = E0999)] -pub(super) struct InvalidConstructorSpread { - #[primary_span] - pub(super) span: Span, -} - #[derive(Diagnostic)] #[diag(desugar_invalid_dot_var, code = E0999)] pub(super) struct InvalidDotVar { @@ -127,7 +120,7 @@ pub(super) struct MultipleSpreadsInConstructor { } impl MultipleSpreadsInConstructor { - pub(super) fn new(path: &surface::ExprPath, prev_path: &surface::ExprPath) -> Self { - Self { span: path.span, prev_span: prev_path.span } + pub(super) fn new(span: Span, prev_span: Span) -> Self { + Self { span, prev_span } } } diff --git a/crates/flux-desugar/src/resolver/refinement_resolver.rs b/crates/flux-desugar/src/resolver/refinement_resolver.rs index f037b7685a..2beec71d2a 100644 --- a/crates/flux-desugar/src/resolver/refinement_resolver.rs +++ b/crates/flux-desugar/src/resolver/refinement_resolver.rs @@ -7,7 +7,7 @@ use flux_middle::{ ResolverOutput, }; use flux_syntax::{ - surface::{self, visit::Visitor as _, ConstructorArgs, Ident, NodeId}, + surface::{self, visit::Visitor as _, Ident, NodeId}, walk_list, }; use rustc_data_structures::{ @@ -296,18 +296,8 @@ impl surface::visit::Visitor for ScopedVisitorWrapper { self.on_func(*func, expr.node_id); } surface::ExprKind::Dot(path, _) => self.on_path(path), - surface::ExprKind::Constructor(path, args) => { - // walk constructor path + surface::ExprKind::Constructor(path, _) => { self.on_path(path); - // walk spread if there is one - args.iter() - .filter_map(|arg| { - match arg { - ConstructorArgs::FieldExpr(_) => None, - ConstructorArgs::Spread(s) => Some(s), - } - }) - .for_each(|arg| self.on_path(&arg.path)); } _ => {} } diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 4640195fb9..ed57cefa07 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -1639,15 +1639,15 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, P> { struct_def_id: DefId, env: &mut Env, exprs: &[fhir::FieldExpr], - spread: &Option, + spread: &Option<&fhir::Spread>, ) -> QueryResult> { let struct_adt = self.genv.adt_sort_def_of(struct_def_id)?; - let sort_and_idx_by_field = struct_adt.sort_and_idx_by_field_name(); + let sort_by_field = struct_adt.sort_by_field_name(); let mut used_fields = FxHashSet::default(); let mut assns = Vec::new(); for expr_val in exprs { let field_symbol = expr_val.ident.name; - if let Some((idx, _)) = sort_and_idx_by_field.get(&field_symbol) { + if let Some(idx) = sort_by_field.get_index_of(&field_symbol) { assns.push((self.conv_expr(env, &expr_val.expr)?, idx)) } used_fields.replace(field_symbol); @@ -1656,27 +1656,16 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, P> { // compute the unused fields and // create projections from unused fields // and push them into assignments - sort_and_idx_by_field + let spread_expr = self.conv_expr(env, &spread.expr)?; + sort_by_field .iter() - .filter_map(|(fld, (idx, _))| { + .enumerate() + .filter_map(|(idx, (fld, _))| { match used_fields.get(fld) { None => { - match spread.path.res { - ExprRes::Param(..) => { - let expr = env.lookup(&spread.path).to_expr(); - let proj = rty::FieldProj::Adt { - def_id: struct_def_id, - field: *idx as u32, - }; - Some((rty::Expr::field_proj(expr, proj), idx)) - } - _ => { - span_bug!( - spread.span, - "unexpected path in constructor's spread after desugaring" - ) - } - } + let proj = + rty::FieldProj::Adt { def_id: struct_def_id, field: idx as u32 }; + Some((rty::Expr::field_proj(spread_expr.clone(), proj), idx)) } Some(_) => None, } diff --git a/crates/flux-fhir-analysis/src/wf/sortck.rs b/crates/flux-fhir-analysis/src/wf/sortck.rs index 0cb2c08f35..c9ee5deace 100644 --- a/crates/flux-fhir-analysis/src/wf/sortck.rs +++ b/crates/flux-fhir-analysis/src/wf/sortck.rs @@ -88,7 +88,7 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { &mut self, expr_span: Span, field_exprs: &[fhir::FieldExpr], - spread: &Option, + spread: &Option<&fhir::Spread>, expected: &rty::Sort, ) -> Result { if let rty::Sort::App(rty::SortCtor::Adt(sort_def), _) = expected { @@ -112,20 +112,7 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { } if let Some(spread) = spread { // must check that the spread is of the same sort as the constructor - match spread.path.res { - ExprRes::Param(_, id) => { - let found = self.param_sort(id); - if !self.is_coercible(&found, expected, spread.fhir_id) { - return Err(self.emit_sort_mismatch(spread.span, &expected, &found)); - } - } - _ => { - span_bug!( - spread.span, - "unexpected path in constructor's spread after desugaring" - ) - } - } + self.check_expr(&spread.expr, expected)?; Ok(()) } else if sort_by_field_name.len() != used_fields.len() { // emit an error because all fields are not used diff --git a/crates/flux-middle/src/fhir.rs b/crates/flux-middle/src/fhir.rs index 901c48ba19..ee83b8dd67 100644 --- a/crates/flux-middle/src/fhir.rs +++ b/crates/flux-middle/src/fhir.rs @@ -911,7 +911,7 @@ pub struct FieldExpr<'fhir> { #[derive(Debug, Clone, Copy)] pub struct Spread<'fhir> { - pub path: PathExpr<'fhir>, + pub expr: Expr<'fhir>, pub span: Span, pub fhir_id: FhirId, } @@ -935,7 +935,7 @@ pub enum ExprKind<'fhir> { IfThenElse(&'fhir Expr<'fhir>, &'fhir Expr<'fhir>, &'fhir Expr<'fhir>), Abs(&'fhir [RefineParam<'fhir>], &'fhir Expr<'fhir>), Record(&'fhir [Expr<'fhir>]), - Constructor(PathExpr<'fhir>, &'fhir [FieldExpr<'fhir>], Option>), + Constructor(PathExpr<'fhir>, &'fhir [FieldExpr<'fhir>], Option<&'fhir Spread<'fhir>>), } impl<'fhir> Expr<'fhir> { diff --git a/crates/flux-middle/src/fhir/visit.rs b/crates/flux-middle/src/fhir/visit.rs index 6371e3e1a0..065a4bcfa4 100644 --- a/crates/flux-middle/src/fhir/visit.rs +++ b/crates/flux-middle/src/fhir/visit.rs @@ -496,7 +496,7 @@ pub fn walk_expr<'v, V: Visitor<'v>>(vis: &mut V, expr: &Expr<'v>) { vis.visit_path_expr(&path); walk_list!(vis, visit_field_expr, exprs); if let Some(s) = spread { - vis.visit_path_expr(&s.path); + vis.visit_expr(&s.expr); } } } diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 8219f1b712..557f8f365b 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -14,7 +14,7 @@ mod pretty; pub mod projections; pub mod refining; pub mod subst; -use std::{borrow::Cow, cmp::Ordering, collections::HashMap, hash::Hash, iter, sync::LazyLock}; +use std::{borrow::Cow, cmp::Ordering, hash::Hash, iter, sync::LazyLock}; pub use binder::{Binder, BoundReftKind, BoundVariableKind, BoundVariableKinds, EarlyBinder}; pub use evars::{EVar, EVarGen}; @@ -39,8 +39,7 @@ use flux_rustc_bridge::{ }; use itertools::Itertools; pub use normalize::SpecFuncDefns; -use rustc_data_structures::unord::UnordMap; -use rustc_hash::FxHashMap; +use rustc_data_structures::{fx::FxIndexMap, unord::UnordMap}; use rustc_hir::{def_id::DefId, LangItem, Safety}; use rustc_index::{newtype_index, IndexSlice}; use rustc_macros::{extension, Decodable, Encodable, TyDecodable, TyEncodable}; @@ -115,8 +114,8 @@ impl AdtSortDef { &self.0.field_names } - pub fn sort_by_field_name(&self) -> FxHashMap { - let mut map = FxHashMap::default(); + pub fn sort_by_field_name(&self) -> FxIndexMap { + let mut map = FxIndexMap::default(); self.0 .sorts .iter() @@ -127,19 +126,6 @@ impl AdtSortDef { map } - pub fn sort_and_idx_by_field_name(&self) -> HashMap { - let mut map = HashMap::new(); - self.0 - .sorts - .iter() - .zip(self.0.field_names.iter()) - .enumerate() - .for_each(|(idx, (sort, field_name))| { - map.insert(*field_name, (idx, sort)); - }); - map - } - pub fn field_by_name(&self, args: &[Sort], name: Symbol) -> Option<(FieldProj, Sort)> { let idx = self.0.field_names.iter().position(|it| name == *it)?; let proj = FieldProj::Adt { def_id: self.did(), field: idx as u32 }; diff --git a/crates/flux-syntax/src/grammar.lalrpop b/crates/flux-syntax/src/grammar.lalrpop index 46578f370b..845fa80249 100644 --- a/crates/flux-syntax/src/grammar.lalrpop +++ b/crates/flux-syntax/src/grammar.lalrpop @@ -562,9 +562,9 @@ ConstructorArgs: surface::ConstructorArgs = { span: cx.map_span(lo, hi) }) }, - ".." => { + ".." > => { surface::ConstructorArgs::Spread(surface::Spread { - path: spread, + expr: spread, node_id: cx.next_node_id(), span: cx.map_span(lo, hi) }) diff --git a/crates/flux-syntax/src/surface.rs b/crates/flux-syntax/src/surface.rs index a2745cdba9..15da494094 100644 --- a/crates/flux-syntax/src/surface.rs +++ b/crates/flux-syntax/src/surface.rs @@ -456,7 +456,7 @@ pub struct FieldExpr { #[derive(Debug)] pub struct Spread { - pub path: ExprPath, + pub expr: Expr, pub span: Span, pub node_id: NodeId, } diff --git a/crates/flux-syntax/src/surface/visit.rs b/crates/flux-syntax/src/surface/visit.rs index a83f93e60c..77313b9188 100644 --- a/crates/flux-syntax/src/surface/visit.rs +++ b/crates/flux-syntax/src/surface/visit.rs @@ -156,7 +156,7 @@ pub trait Visitor: Sized { fn visit_constructor_args(&mut self, expr: &ConstructorArgs) { match expr { ConstructorArgs::FieldExpr(field_expr) => walk_field_expr(self, field_expr), - ConstructorArgs::Spread(spread) => walk_path_expr(self, &spread.path), + ConstructorArgs::Spread(spread) => self.visit_expr(&spread.expr), } } diff --git a/tests/tests/pos/constructors/test04.rs b/tests/tests/pos/constructors/test04.rs new file mode 100644 index 0000000000..cbc142721e --- /dev/null +++ b/tests/tests/pos/constructors/test04.rs @@ -0,0 +1,23 @@ +#![flux::defs { + fn some_computation(s: S) -> S { s } +}] + +#[flux::refined_by(x: int, y: int)] +pub struct S { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +impl S { + #[flux::sig(fn (self: &strg S[@old_x]) ensures self: S[S { x: 1, ..some_computation(old_x) }])] + pub fn update(&mut self) { + self.x = 1; + } + + #[flux::sig(fn (self: &strg S[@old_x]) ensures self: S[S { x: 1, ..S { x: 2, ..old_x } }])] + pub fn update2(&mut self) { + self.x = 1; + } +} From 49553b6212018608e62dc421fb81723b8d0ea5ac Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Tue, 19 Nov 2024 11:15:29 -0800 Subject: [PATCH 12/15] fix merge conflicts --- crates/flux-middle/src/rty/mod.rs | 3 +-- crates/flux-syntax/src/surface/visit.rs | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index e7ae15deaa..30f64b642b 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -40,9 +40,8 @@ use flux_rustc_bridge::{ }; use itertools::Itertools; pub use normalize::SpecFuncDefns; -use rustc_data_structures::{fx::FxIndexMap, unord::UnordMap}; use refining::Refiner; -use rustc_data_structures::unord::UnordMap; +use rustc_data_structures::{fx::FxIndexMap, unord::UnordMap}; use rustc_hir::{def_id::DefId, LangItem, Safety}; use rustc_index::{newtype_index, IndexSlice}; use rustc_macros::{extension, Decodable, Encodable, TyDecodable, TyEncodable}; diff --git a/crates/flux-syntax/src/surface/visit.rs b/crates/flux-syntax/src/surface/visit.rs index 24533e10de..bfb2379eff 100644 --- a/crates/flux-syntax/src/surface/visit.rs +++ b/crates/flux-syntax/src/surface/visit.rs @@ -1,7 +1,7 @@ use rustc_span::symbol::Ident; use super::{ - AliasReft, ArrayLen, Async, BaseSort, BaseTy, BaseTyKind, ConstructorArgs, Ensures, EnumDef, + AliasReft, Async, BaseSort, BaseTy, BaseTyKind, ConstArg, ConstructorArgs, Ensures, EnumDef, Expr, ExprKind, ExprPath, ExprPathSegment, FieldExpr, FnInput, FnOutput, FnRetTy, FnSig, GenericArg, GenericArgKind, GenericParam, Generics, Impl, ImplAssocReft, Indices, Lit, Path, PathSegment, Qualifier, RefineArg, RefineParam, Sort, SortPath, SpecFunc, StructDef, Trait, From 2f667d5ce6fcb41dd3eed1034e3e4f8a3c962891 Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Tue, 19 Nov 2024 16:09:10 -0800 Subject: [PATCH 13/15] Handle constructor generics --- crates/flux-fhir-analysis/src/wf/sortck.rs | 12 ++++++------ crates/flux-middle/src/rty/mod.rs | 19 ++++++++++++------- .../neg/error_messages/wf/constructor06.rs | 12 ++++++++++++ tests/tests/pos/constructors/test05.rs | 17 +++++++++++++++++ tests/tests/pos/constructors/test06.rs | 14 ++++++++++++++ 5 files changed, 61 insertions(+), 13 deletions(-) create mode 100644 tests/tests/neg/error_messages/wf/constructor06.rs create mode 100644 tests/tests/pos/constructors/test05.rs create mode 100644 tests/tests/pos/constructors/test06.rs diff --git a/crates/flux-fhir-analysis/src/wf/sortck.rs b/crates/flux-fhir-analysis/src/wf/sortck.rs index 75c2b2497e..01dc38a2f9 100644 --- a/crates/flux-fhir-analysis/src/wf/sortck.rs +++ b/crates/flux-fhir-analysis/src/wf/sortck.rs @@ -91,14 +91,14 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { spread: &Option<&fhir::Spread>, expected: &rty::Sort, ) -> Result { - if let rty::Sort::App(rty::SortCtor::Adt(sort_def), _) = expected { - let sort_by_field_name = sort_def.sort_by_field_name(); + let expected = self.resolve_vars_if_possible(expected); + if let rty::Sort::App(rty::SortCtor::Adt(sort_def), sort_args) = &expected { + let sort_by_field_name = sort_def.sort_by_field_name_subst(&sort_args); let mut used_fields = FxHashSet::default(); - for expr in field_exprs { // make sure that the field is actually a field if let Some(sort) = sort_by_field_name.get(&expr.ident.name) { - self.check_expr(&expr.expr, sort)?; + self.check_expr(&expr.expr, &sort)?; } else { return Err( self.emit_err(errors::FieldNotFound::new(expected.clone(), expr.ident)) @@ -112,7 +112,7 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { } if let Some(spread) = spread { // must check that the spread is of the same sort as the constructor - self.check_expr(&spread.expr, expected)?; + self.check_expr(&spread.expr, &expected)?; Ok(()) } else if sort_by_field_name.len() != used_fields.len() { // emit an error because all fields are not used @@ -128,7 +128,7 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { Ok(()) } } else { - Err(self.emit_err(errors::UnexpectedConstructor::new(expr_span, expected))) + Err(self.emit_err(errors::UnexpectedConstructor::new(expr_span, &expected))) } } diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 30f64b642b..2be5830ae6 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -118,13 +118,18 @@ impl AdtSortDef { pub fn sort_by_field_name(&self) -> FxIndexMap { let mut map = FxIndexMap::default(); - self.0 - .sorts - .iter() - .zip(self.0.field_names.iter()) - .for_each(|(sort, field_name)| { - map.insert(*field_name, sort); - }); + std::iter::zip(self.0.sorts.iter(), self.0.field_names.iter()).for_each(|(sort, field_name)| { + map.insert(*field_name, sort); + }); + map + } + + pub fn sort_by_field_name_subst(&self, args: &[Sort]) -> FxIndexMap { + let mut map = FxIndexMap::default(); + let folded = self.0.sorts.fold_with(&mut SortSubst::new(args)); + std::iter::zip(folded.iter(), self.0.field_names.iter()).for_each(|(sort, field_name)| { + map.insert(*field_name, sort.clone()); + }); map } diff --git a/tests/tests/neg/error_messages/wf/constructor06.rs b/tests/tests/neg/error_messages/wf/constructor06.rs new file mode 100644 index 0000000000..73d51e5cda --- /dev/null +++ b/tests/tests/neg/error_messages/wf/constructor06.rs @@ -0,0 +1,12 @@ +use flux_rs::*; + +#[flux::refined_by(start: T, end: T)] +struct Range { + #[flux::field(T[start])] + pub start: T, + #[flux::field(T[end])] + pub end: T, +} + +#[sig(fn(r: Range{v: v == Range { start: true, end: false } }))] //~ERROR mismatched sorts +fn foo2(_r: Range) {} diff --git a/tests/tests/pos/constructors/test05.rs b/tests/tests/pos/constructors/test05.rs new file mode 100644 index 0000000000..c59e9bbc8f --- /dev/null +++ b/tests/tests/pos/constructors/test05.rs @@ -0,0 +1,17 @@ +use flux_rs::*; + +#[flux::refined_by(start: T, end: T)] +struct Range { + #[flux::field(T[start])] + pub start: T, + #[flux::field(T[end])] + pub end: T, +} + +#[flux::sig(fn(r: Range[@old]) -> Range[ Range { ..old } ])] +fn foo(r: Range) -> Range { + r +} + +#[sig(fn(r: Range{v: v == Range { start: 0, end: 0 } }))] +fn foo2(_r: Range) {} diff --git a/tests/tests/pos/constructors/test06.rs b/tests/tests/pos/constructors/test06.rs new file mode 100644 index 0000000000..00405adaf3 --- /dev/null +++ b/tests/tests/pos/constructors/test06.rs @@ -0,0 +1,14 @@ +#[flux::refined_by(b: bool, y: int)] +pub struct S { + #[flux::field(bool[b])] + b: bool, + #[flux::field(u32[y])] + y: u32, +} + +#[flux::sig(fn (S[@old_s]) -> S[S { y: 2, b: true }])] +fn f(mut s: S) -> S { + s.b = true; + s.y = 2; + s +} From 0f9fa2516aa2d102fe08922dac4378655ea94e27 Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Tue, 19 Nov 2024 17:28:09 -0800 Subject: [PATCH 14/15] Handle sort checking path of constuctor --- crates/flux-fhir-analysis/locales/en-US.ftl | 5 + crates/flux-fhir-analysis/src/conv/mod.rs | 6 +- crates/flux-fhir-analysis/src/wf/errors.rs | 15 +++ crates/flux-fhir-analysis/src/wf/sortck.rs | 96 +++++++++++-------- crates/flux-middle/src/rty/mod.rs | 10 +- .../neg/error_messages/wf/constructor07.rs | 22 +++++ 6 files changed, 104 insertions(+), 50 deletions(-) create mode 100644 tests/tests/neg/error_messages/wf/constructor07.rs diff --git a/crates/flux-fhir-analysis/locales/en-US.ftl b/crates/flux-fhir-analysis/locales/en-US.ftl index 46b00fee5b..d598fa478f 100644 --- a/crates/flux-fhir-analysis/locales/en-US.ftl +++ b/crates/flux-fhir-analysis/locales/en-US.ftl @@ -3,6 +3,11 @@ fhir_analysis_sort_mismatch = mismatched sorts .label = expected `{$expected}`, found `{$found}` + +fhir_analysis_sort_mismatch_found_omitted = + mismatched sorts + .label = expected `{$expected}` + fhir_analysis_arg_count_mismatch = this {$thing} takes {$expected -> [one] {$expected} refinement argument diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 0aef5acef0..d44e510660 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -27,7 +27,7 @@ use flux_middle::{ }; use flux_rustc_bridge::{lowering::Lower, ToRustc}; use itertools::Itertools; -use rustc_data_structures::fx::FxIndexMap; +use rustc_data_structures::fx::{FxIndexMap, FxIndexSet}; use rustc_errors::Diagnostic; use rustc_hash::FxHashSet; use rustc_hir::{ @@ -1666,7 +1666,7 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, P> { spread: &Option<&fhir::Spread>, ) -> QueryResult> { let struct_adt = self.genv.adt_sort_def_of(struct_def_id)?; - let sort_by_field = struct_adt.sort_by_field_name(); + let sort_by_field = FxIndexSet::from_iter(struct_adt.field_names()); let mut used_fields = FxHashSet::default(); let mut assns = Vec::new(); for expr_val in exprs { @@ -1684,7 +1684,7 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, P> { sort_by_field .iter() .enumerate() - .filter_map(|(idx, (fld, _))| { + .filter_map(|(idx, fld)| { match used_fields.get(fld) { None => { let proj = diff --git a/crates/flux-fhir-analysis/src/wf/errors.rs b/crates/flux-fhir-analysis/src/wf/errors.rs index cb9a99b944..19791e4fad 100644 --- a/crates/flux-fhir-analysis/src/wf/errors.rs +++ b/crates/flux-fhir-analysis/src/wf/errors.rs @@ -19,6 +19,21 @@ impl SortMismatch { } } +#[derive(Diagnostic)] +#[diag(fhir_analysis_sort_mismatch_found_omitted, code = E0999)] +pub(super) struct SortMismatchFoundOmitted { + #[primary_span] + #[label] + span: Span, + expected: rty::Sort, +} + +impl SortMismatchFoundOmitted { + pub(super) fn new(span: Span, expected: rty::Sort) -> Self { + Self { span, expected } + } +} + #[derive(Diagnostic)] #[diag(fhir_analysis_arg_count_mismatch, code = E0999)] pub(super) struct ArgCountMismatch { diff --git a/crates/flux-fhir-analysis/src/wf/sortck.rs b/crates/flux-fhir-analysis/src/wf/sortck.rs index 01dc38a2f9..d065785703 100644 --- a/crates/flux-fhir-analysis/src/wf/sortck.rs +++ b/crates/flux-fhir-analysis/src/wf/sortck.rs @@ -4,13 +4,13 @@ use ena::unify::InPlaceUnificationTable; use flux_common::{bug, iter::IterExt, result::ResultExt, span_bug, tracked_span_bug}; use flux_errors::{ErrorGuaranteed, Errors}; use flux_middle::{ - fhir::{self, visit::Visitor as _, ExprRes, FhirId, FluxOwnerId}, + fhir::{self, visit::Visitor as _, ExprRes, FhirId, FluxOwnerId, PathExpr}, global_env::GlobalEnv, queries::QueryResult, rty::{ self, fold::{FallibleTypeFolder, TypeFoldable, TypeFolder, TypeSuperFoldable}, - WfckResults, + AdtSortDef, WfckResults, }, }; use itertools::{izip, Itertools}; @@ -84,49 +84,68 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { } } - fn check_constructor( + fn check_field_exprs( &mut self, expr_span: Span, + sort_def: &AdtSortDef, + sort_args: &[rty::Sort], field_exprs: &[fhir::FieldExpr], spread: &Option<&fhir::Spread>, expected: &rty::Sort, ) -> Result { - let expected = self.resolve_vars_if_possible(expected); - if let rty::Sort::App(rty::SortCtor::Adt(sort_def), sort_args) = &expected { - let sort_by_field_name = sort_def.sort_by_field_name_subst(&sort_args); - let mut used_fields = FxHashSet::default(); - for expr in field_exprs { - // make sure that the field is actually a field - if let Some(sort) = sort_by_field_name.get(&expr.ident.name) { - self.check_expr(&expr.expr, &sort)?; - } else { - return Err( - self.emit_err(errors::FieldNotFound::new(expected.clone(), expr.ident)) - ); - } - if let Some(old_field) = used_fields.replace(expr.ident) { - return Err( - self.emit_err(errors::DuplicateFieldUsed::new(expr.ident, old_field)) - ); - } + let sort_by_field_name = sort_def.sort_by_field_name(&sort_args); + let mut used_fields = FxHashSet::default(); + for expr in field_exprs { + // make sure that the field is actually a field + if let Some(sort) = sort_by_field_name.get(&expr.ident.name) { + self.check_expr(&expr.expr, &sort)?; + } else { + return Err(self.emit_err(errors::FieldNotFound::new(expected.clone(), expr.ident))); } - if let Some(spread) = spread { - // must check that the spread is of the same sort as the constructor - self.check_expr(&spread.expr, &expected)?; - Ok(()) - } else if sort_by_field_name.len() != used_fields.len() { - // emit an error because all fields are not used - let used_field_names: Vec = - used_fields.into_iter().map(|k| k.name).collect(); - let fields_remaining = sort_by_field_name - .into_keys() - .filter(|x| !used_field_names.contains(x)) - .collect(); + if let Some(old_field) = used_fields.replace(expr.ident) { + return Err(self.emit_err(errors::DuplicateFieldUsed::new(expr.ident, old_field))); + } + } + if let Some(spread) = spread { + // must check that the spread is of the same sort as the constructor + self.check_expr(&spread.expr, expected)?; + Ok(()) + } else if sort_by_field_name.len() != used_fields.len() { + // emit an error because all fields are not used + let used_field_names: Vec = + used_fields.into_iter().map(|k| k.name).collect(); + let fields_remaining = sort_by_field_name + .into_keys() + .filter(|x| !used_field_names.contains(x)) + .collect(); + return Err( + self.emit_err(errors::ConstructorMissingFields::new(expr_span, fields_remaining)) + ); + } else { + Ok(()) + } + } + + fn check_constructor( + &mut self, + expr_span: Span, + path: &PathExpr, + field_exprs: &[fhir::FieldExpr], + spread: &Option<&fhir::Spread>, + expected: &rty::Sort, + ) -> Result { + if let rty::Sort::App(rty::SortCtor::Adt(sort_def), sort_args) = expected { + let expected_def_id = sort_def.did(); + let path_def_id = match path.res { + ExprRes::Struct(def_id) | ExprRes::Enum(def_id) => def_id, + _ => span_bug!(expr_span, "unexpected path in constructor"), + }; + if path_def_id != expected_def_id { return Err(self - .emit_err(errors::ConstructorMissingFields::new(expr_span, fields_remaining))); - } else { - Ok(()) + .emit_err(errors::SortMismatchFoundOmitted::new(path.span, expected.clone()))); } + self.check_field_exprs(expr_span, sort_def, sort_args, field_exprs, spread, expected)?; + Ok(()) } else { Err(self.emit_err(errors::UnexpectedConstructor::new(expr_span, &expected))) } @@ -190,8 +209,9 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { self.check_abs(expr, refine_params, body, expected)?; } fhir::ExprKind::Record(fields) => self.check_record(expr, fields, expected)?, - fhir::ExprKind::Constructor(_path, exprs, spread) => { - self.check_constructor(expr.span, exprs, spread, expected)? + fhir::ExprKind::Constructor(path, exprs, spread) => { + let expected = self.resolve_vars_if_possible(expected); + self.check_constructor(expr.span, path, exprs, spread, &expected)?; } } Ok(()) diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 2be5830ae6..3f4f466d8f 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -116,15 +116,7 @@ impl AdtSortDef { &self.0.field_names } - pub fn sort_by_field_name(&self) -> FxIndexMap { - let mut map = FxIndexMap::default(); - std::iter::zip(self.0.sorts.iter(), self.0.field_names.iter()).for_each(|(sort, field_name)| { - map.insert(*field_name, sort); - }); - map - } - - pub fn sort_by_field_name_subst(&self, args: &[Sort]) -> FxIndexMap { + pub fn sort_by_field_name(&self, args: &[Sort]) -> FxIndexMap { let mut map = FxIndexMap::default(); let folded = self.0.sorts.fold_with(&mut SortSubst::new(args)); std::iter::zip(folded.iter(), self.0.field_names.iter()).for_each(|(sort, field_name)| { diff --git a/tests/tests/neg/error_messages/wf/constructor07.rs b/tests/tests/neg/error_messages/wf/constructor07.rs new file mode 100644 index 0000000000..95877502ee --- /dev/null +++ b/tests/tests/neg/error_messages/wf/constructor07.rs @@ -0,0 +1,22 @@ +#[flux::refined_by(x: int, y: int)] +struct S1 { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +#[flux::refined_by(x: int, y: int)] +struct S2 { + #[flux::field(u32[x])] + x: u32, + #[flux::field(u32[y])] + y: u32, +} + +#[flux::sig(fn (S1[@s1]) -> S1[S2 { x: 1, y: 2 }])] //~ERROR mismatched sorts +fn foo(mut s1: S1) -> S1 { + s1.x = 1; + s1.y = 2; + s1 +} From 58e86f58376f249a5c540673e2baa87ca6ae4785 Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Wed, 20 Nov 2024 10:58:57 -0800 Subject: [PATCH 15/15] Style changes --- crates/flux-desugar/src/desugar.rs | 32 ++++++++--------- crates/flux-fhir-analysis/src/conv/mod.rs | 43 +++++++---------------- crates/flux-middle/src/rty/mod.rs | 9 ++--- 3 files changed, 32 insertions(+), 52 deletions(-) diff --git a/crates/flux-desugar/src/desugar.rs b/crates/flux-desugar/src/desugar.rs index 4be9c7b677..fa7dfd0ecb 100644 --- a/crates/flux-desugar/src/desugar.rs +++ b/crates/flux-desugar/src/desugar.rs @@ -1361,22 +1361,22 @@ trait DesugarCtxt<'genv, 'tcx: 'genv> { }) .collect::>(); - let spread = if spreads.len() == 0 { - None - } else if spreads.len() == 1 { - let s = spreads[0]; - let spread = fhir::Spread { - expr: self.desugar_expr(&s.expr)?, - span: s.span, - fhir_id: self.next_fhir_id(), - }; - Some(self.genv().alloc(spread)) - } else { - // Multiple spreads found - emit and error - return Err(self.emit_err(errors::MultipleSpreadsInConstructor::new( - spreads[1].span, - spreads[0].span, - ))); + let spread = match &spreads[..] { + [] => None, + [s] => { + let spread = fhir::Spread { + expr: self.desugar_expr(&s.expr)?, + span: s.span, + fhir_id: self.next_fhir_id(), + }; + Some(self.genv().alloc(spread)) + } + [s1, s2, ..] => { + // Multiple spreads found - emit an error + return Err(self.emit_err(errors::MultipleSpreadsInConstructor::new( + s1.span, s2.span, + ))); + } }; fhir::ExprKind::Constructor(path, field_exprs, spread) } diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index d44e510660..015037936e 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -27,7 +27,7 @@ use flux_middle::{ }; use flux_rustc_bridge::{lowering::Lower, ToRustc}; use itertools::Itertools; -use rustc_data_structures::fx::{FxIndexMap, FxIndexSet}; +use rustc_data_structures::fx::FxIndexMap; use rustc_errors::Diagnostic; use rustc_hash::FxHashSet; use rustc_hir::{ @@ -1666,38 +1666,21 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, P> { spread: &Option<&fhir::Spread>, ) -> QueryResult> { let struct_adt = self.genv.adt_sort_def_of(struct_def_id)?; - let sort_by_field = FxIndexSet::from_iter(struct_adt.field_names()); - let mut used_fields = FxHashSet::default(); + let spread = spread + .map(|spread| self.conv_expr(env, &spread.expr)) + .transpose()?; + let field_exprs_by_name: FxIndexMap = + exprs.iter().map(|e| (e.ident.name, e)).collect(); let mut assns = Vec::new(); - for expr_val in exprs { - let field_symbol = expr_val.ident.name; - if let Some(idx) = sort_by_field.get_index_of(&field_symbol) { - assns.push((self.conv_expr(env, &expr_val.expr)?, idx)) + for (idx, field_name) in struct_adt.field_names().iter().enumerate() { + if let Some(field_expr) = field_exprs_by_name.get(field_name) { + assns.push(self.conv_expr(env, &field_expr.expr)?); + } else if let Some(spread) = &spread { + let proj = rty::FieldProj::Adt { def_id: struct_def_id, field: idx as u32 }; + assns.push(rty::Expr::field_proj(spread, proj)); } - used_fields.replace(field_symbol); } - if let Some(spread) = spread { - // compute the unused fields and - // create projections from unused fields - // and push them into assignments - let spread_expr = self.conv_expr(env, &spread.expr)?; - sort_by_field - .iter() - .enumerate() - .filter_map(|(idx, fld)| { - match used_fields.get(fld) { - None => { - let proj = - rty::FieldProj::Adt { def_id: struct_def_id, field: idx as u32 }; - Some((rty::Expr::field_proj(spread_expr.clone(), proj), idx)) - } - Some(_) => None, - } - }) - .for_each(|proj| assns.push(proj)); - } - assns.sort_by(|lhs, rhs| lhs.1.cmp(&rhs.1)); - Ok(assns.into_iter().map(|x| x.0).collect()) + Ok(List::from_vec(assns)) } fn conv_exprs(&mut self, env: &mut Env, exprs: &[fhir::Expr]) -> QueryResult> { diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 3f4f466d8f..0ea912a980 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -117,12 +117,9 @@ impl AdtSortDef { } pub fn sort_by_field_name(&self, args: &[Sort]) -> FxIndexMap { - let mut map = FxIndexMap::default(); - let folded = self.0.sorts.fold_with(&mut SortSubst::new(args)); - std::iter::zip(folded.iter(), self.0.field_names.iter()).for_each(|(sort, field_name)| { - map.insert(*field_name, sort.clone()); - }); - map + std::iter::zip(&self.0.field_names, &self.0.sorts.fold_with(&mut SortSubst::new(args))) + .map(|(name, sort)| (*name, sort.clone())) + .collect() } pub fn field_by_name(&self, args: &[Sort], name: Symbol) -> Option<(FieldProj, Sort)> {